Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > uniexg | GIF version |
Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent 𝐴 ∈ 𝑉 instead of 𝐴 ∈ V to make the theorem more general and thus shorten some proofs; obviously the universal class constant V is one possible substitution for class variable 𝑉. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
uniexg | ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unieq 3740 | . . 3 ⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴) | |
2 | 1 | eleq1d 2206 | . 2 ⊢ (𝑥 = 𝐴 → (∪ 𝑥 ∈ V ↔ ∪ 𝐴 ∈ V)) |
3 | vex 2684 | . . 3 ⊢ 𝑥 ∈ V | |
4 | 3 | uniex 4354 | . 2 ⊢ ∪ 𝑥 ∈ V |
5 | 2, 4 | vtoclg 2741 | 1 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ∈ wcel 1480 Vcvv 2681 ∪ cuni 3731 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-sep 4041 ax-un 4350 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-rex 2420 df-v 2683 df-uni 3732 |
This theorem is referenced by: abnexg 4362 snnex 4364 uniexb 4389 ssonuni 4399 dmexg 4798 rnexg 4799 elxp4 5021 elxp5 5022 relrnfvex 5432 fvexg 5433 sefvex 5435 riotaexg 5727 iunexg 6010 1stvalg 6033 2ndvalg 6034 cnvf1o 6115 brtpos2 6141 tfrlemiex 6221 tfr1onlemex 6237 tfrcllemex 6250 en1bg 6687 en1uniel 6691 fival 6851 suplocexprlem2b 7515 suplocexprlemlub 7525 restid 12120 istopon 12169 tgval 12207 tgvalex 12208 eltg 12210 eltg2 12211 tgss2 12237 ntrval 12268 restin 12334 cnovex 12354 cnprcl2k 12364 cnptopresti 12396 cnptoprest 12397 cnptoprest2 12398 lmtopcnp 12408 txbasex 12415 uptx 12432 reldvg 12806 |
Copyright terms: Public domain | W3C validator |