![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > prexg | GIF version |
Description: The Axiom of Pairing using class variables. Theorem 7.13 of [Quine] p. 51, but restricted to classes which exist. For proper classes, see prprc 3703, prprc1 3701, and prprc2 3702. (Contributed by Jim Kingdon, 16-Sep-2018.) |
Ref | Expression |
---|---|
prexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | preq2 3671 | . . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵}) | |
2 | 1 | eleq1d 2246 | . . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V)) |
3 | zfpair2 4211 | . . . . 5 ⊢ {𝑥, 𝑦} ∈ V | |
4 | 2, 3 | vtoclg 2798 | . . . 4 ⊢ (𝐵 ∈ 𝑊 → {𝑥, 𝐵} ∈ V) |
5 | preq1 3670 | . . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵}) | |
6 | 5 | eleq1d 2246 | . . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V)) |
7 | 4, 6 | imbitrid 154 | . . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V)) |
8 | 7 | vtocleg 2809 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐵 ∈ 𝑊 → {𝐴, 𝐵} ∈ V)) |
9 | 8 | imp 124 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1353 ∈ wcel 2148 Vcvv 2738 {cpr 3594 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4122 ax-pr 4210 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2740 df-un 3134 df-sn 3599 df-pr 3600 |
This theorem is referenced by: prelpwi 4215 opexg 4229 opi2 4234 opth 4238 opeqsn 4253 opeqpr 4254 uniop 4256 unex 4442 tpexg 4445 op1stb 4479 op1stbg 4480 onun2 4490 opthreg 4556 relop 4778 acexmidlemv 5873 pr2ne 7191 exmidonfinlem 7192 exmidaclem 7207 sup3exmid 8914 xrex 9856 2strbasg 12578 2stropg 12579 prdsex 12718 xpsfval 12767 xpsval 12771 isomninnlem 14781 trilpolemlt1 14792 iswomninnlem 14800 iswomni0 14802 ismkvnnlem 14803 |
Copyright terms: Public domain | W3C validator |