![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniexd | Structured version Visualization version GIF version |
Description: Deduction version of the ZF Axiom of Union in class notation. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
uniexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
Ref | Expression |
---|---|
uniexd | ⊢ (𝜑 → ∪ 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
2 | uniexg 7753 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 Vcvv 3462 ∪ cuni 4915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5306 ax-un 7748 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-ss 3964 df-uni 4916 |
This theorem is referenced by: iunexg 7979 cofon1 8704 cofon2 8705 en1bOLD 9062 axdc2lem 10493 ttukeylem3 10556 ghmqusnsglem1 19276 ghmqusnsg 19278 ghmquskerlem1 19279 ghmquskerco 19280 ghmquskerlem3 19282 ghmqusker 19283 frgpcyg 21573 eltg 22954 ntrval 23034 neiptopnei 23130 neitr 23178 cnpresti 23286 cnprest 23287 lmcnp 23302 uptx 23623 cnextcn 24065 isppw 27145 bdayimaon 27726 nosupno 27736 noinfno 27751 noeta2 27817 etasslt2 27847 scutbdaybnd2lim 27850 oldval 27881 elrspunidl 33305 algextdeglem4 33589 braew 34077 omsfval 34130 omssubaddlem 34135 omssubadd 34136 omsmeas 34159 sibfof 34176 isrrvv 34279 rrvmulc 34289 bnj1489 34903 isfne4 36054 topjoin 36079 mbfresfi 37369 supex2g 37440 restuni4 44740 unirnmap 44833 stoweidlem50 45689 stoweidlem57 45696 stoweidlem59 45698 stoweidlem60 45699 fourierdlem71 45816 intsal 45969 subsaluni 45999 caragenval 46132 omecl 46142 issmflem 46366 issmflelem 46383 issmfle 46384 smfconst 46388 issmfgtlem 46394 issmfgt 46395 issmfgelem 46408 issmfge 46409 smfpimioo 46426 smfresal 46427 fundcmpsurinjlem3 46990 iscnrm3rlem7 48298 toplatglb 48345 setrec1lem2 48452 |
Copyright terms: Public domain | W3C validator |