| 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 7760 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 ∪ cuni 4907 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 |
| This theorem is referenced by: unexg 7763 iunexg 7988 cofon1 8710 cofon2 8711 axdc2lem 10488 ttukeylem3 10551 ghmqusnsglem1 19298 ghmqusnsg 19300 ghmquskerlem1 19301 ghmquskerco 19302 ghmquskerlem3 19304 ghmqusker 19305 frgpcyg 21592 eltg 22964 ntrval 23044 neiptopnei 23140 neitr 23188 cnpresti 23296 cnprest 23297 lmcnp 23312 uptx 23633 cnextcn 24075 isppw 27157 bdayimaon 27738 nosupno 27748 noinfno 27763 noeta2 27829 etasslt2 27859 scutbdaybnd2lim 27862 oldval 27893 elrspunidl 33456 algextdeglem4 33761 braew 34243 omsfval 34296 omssubaddlem 34301 omssubadd 34302 omsmeas 34325 sibfof 34342 isrrvv 34445 rrvmulc 34455 bnj1489 35070 isfne4 36341 topjoin 36366 mbfresfi 37673 supex2g 37744 restuni4 45126 unirnmap 45213 stoweidlem50 46065 stoweidlem57 46072 stoweidlem59 46074 stoweidlem60 46075 fourierdlem71 46192 intsal 46345 subsaluni 46375 caragenval 46508 omecl 46518 issmflem 46742 issmflelem 46759 issmfle 46760 smfconst 46764 issmfgtlem 46770 issmfgt 46771 issmfgelem 46784 issmfge 46785 smfpimioo 46802 smfresal 46803 fundcmpsurinjlem3 47387 iscnrm3rlem7 48843 toplatglb 48890 setrec1lem2 49207 |
| Copyright terms: Public domain | W3C validator |