![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniexg | Structured version Visualization version Unicode version |
Description: The ZF Axiom of Union in
class notation, in the form of a theorem
instead of an inference. We use the antecedent ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
uniexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieq 4206 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq1d 2513 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3048 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | uniex 6587 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | vtoclg 3107 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-un 6583 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-rex 2743 df-v 3047 df-uni 4199 |
This theorem is referenced by: snnex 6597 uniexb 6601 ssonuni 6613 ssonprc 6619 dmexg 6724 rnexg 6725 iunexg 6769 undefval 7023 onovuni 7061 tz7.44lem1 7123 tz7.44-3 7126 en1b 7637 en1uniel 7641 disjen 7729 domss2 7731 fival 7926 fipwuni 7940 supexd 7967 cantnflem1 8194 dfac8clem 8463 onssnum 8471 dfac12lem1 8573 dfac12lem2 8574 fin1a2lem12 8841 hsmexlem1 8856 axdc2lem 8878 ttukeylem3 8941 wrdexb 12683 restid 15332 prdsbas 15355 prdsplusg 15356 prdsmulr 15357 prdsvsca 15358 prdshom 15365 sscpwex 15720 pmtrfv 17093 frgpcyg 19144 istopon 19940 tgval 19970 eltg 19972 eltg2 19973 tgss2 20003 ntrval 20051 neiptoptop 20147 neiptopnei 20148 restin 20182 neitr 20196 restntr 20198 cnpresti 20304 cnprest 20305 cnprest2 20306 lmcnp 20320 pnrmopn 20359 cnrmnrm 20377 cmpsublem 20414 cmpsub 20415 cmpcld 20417 hausmapdom 20515 isref 20524 locfindis 20545 txbasex 20581 dfac14lem 20632 uptx 20640 xkopt 20670 xkopjcn 20671 qtopval2 20711 elqtop 20712 fbssfi 20852 ptcmplem2 21068 cnextfval 21077 cnextcn 21082 tuslem 21282 isppw 24041 elpwunicl 28168 acunirnmpt2 28262 acunirnmpt2f 28263 hasheuni 28906 insiga 28959 sigagenval 28962 braew 29065 omsval 29117 omsvalOLD 29121 omssubaddlem 29127 omssubadd 29128 omssubaddlemOLD 29131 omssubaddOLD 29132 omsmeas 29155 omsmeasOLD 29156 sibfof 29173 sitmcl 29184 isrrvv 29276 rrvmulc 29286 bnj1489 29865 kur14 29939 cvmscld 29996 nobndlem1 30581 fobigcup 30667 hfuni 30951 isfne 30995 isfne4b 30997 topjoin 31021 fnemeet1 31022 tailfval 31028 mbfresfi 31987 supex2g 32064 kelac2 35923 cnfex 37349 unidmex 37388 pwpwuni 37397 stoweidlem50 37911 stoweidlem57 37918 stoweidlem59 37920 stoweidlem60 37921 fourierdlem71 38041 salgenval 38182 intsaluni 38188 intsal 38189 salgenn0 38190 caragenval 38314 omecl 38324 caragenunidm 38329 |
Copyright terms: Public domain | W3C validator |