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 7456 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 Vcvv 3492 ∪ cuni 4830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-v 3494 df-uni 4831 |
This theorem is referenced by: iunexg 7653 en1b 8565 axdc2lem 9858 ttukeylem3 9921 frgpcyg 20648 eltg 21493 ntrval 21572 neiptopnei 21668 neitr 21716 cnpresti 21824 cnprest 21825 lmcnp 21840 uptx 22161 cnextcn 22603 isppw 25618 braew 31400 omsfval 31451 omssubaddlem 31456 omssubadd 31457 omsmeas 31480 sibfof 31497 isrrvv 31600 rrvmulc 31610 bnj1489 32225 bdayimaon 33094 nosupno 33100 isfne4 33585 topjoin 33610 mbfresfi 34819 supex2g 34893 restuni4 41264 unirnmap 41347 stoweidlem50 42212 stoweidlem57 42219 stoweidlem59 42221 stoweidlem60 42222 fourierdlem71 42339 intsal 42490 subsaluni 42520 caragenval 42652 omecl 42662 issmflem 42881 issmflelem 42898 issmfle 42899 smfconst 42903 issmfgtlem 42909 issmfgt 42910 issmfgelem 42922 issmfge 42923 smfpimioo 42939 smfresal 42940 fundcmpsurinjlem3 43437 setrec1lem2 44719 |
Copyright terms: Public domain | W3C validator |