Proofgold Proposition

∀ x0 x1 : ι → ι → ο . wceq (ciun x0 x1) (cab (λ x2 . wrex (λ x3 . wcel (cv x2) (x1 x3)) x0))

type
prop

theory
SetMM

name
df_iun

proof
PUQyb..

Megalodon
-

proofgold address
TMH34..

creator
36397 PrCmT../60c4c..

owner
36397 PrCmT../60c4c..

term root
46841..