| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > prexg | Unicode 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 3742, prprc1 3740, and prprc2 3741. (Contributed by Jim Kingdon, 16-Sep-2018.) |
| Ref | Expression |
|---|---|
| prexg |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | preq2 3710 |
. . . . . 6
| |
| 2 | 1 | eleq1d 2273 |
. . . . 5
|
| 3 | zfpair2 4253 |
. . . . 5
| |
| 4 | 2, 3 | vtoclg 2832 |
. . . 4
|
| 5 | preq1 3709 |
. . . . 5
| |
| 6 | 5 | eleq1d 2273 |
. . . 4
|
| 7 | 4, 6 | imbitrid 154 |
. . 3
|
| 8 | 7 | vtocleg 2843 |
. 2
|
| 9 | 8 | imp 124 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| 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 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pr 4252 |
| This theorem depends on definitions: df-bi 117 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-v 2773 df-un 3169 df-sn 3638 df-pr 3639 |
| This theorem is referenced by: prelpwi 4257 opexg 4271 opi2 4276 opth 4280 opeqsn 4296 opeqpr 4297 uniop 4299 unex 4487 tpexg 4490 op1stb 4524 op1stbg 4525 onun2 4537 opthreg 4603 relop 4827 acexmidlemv 5941 en2prd 6908 pw2f1odclem 6930 pr2ne 7299 exmidonfinlem 7300 exmidaclem 7319 sup3exmid 9029 xrex 9977 2strbasg 12923 2stropg 12924 prdsex 13072 prdsval 13076 xpsfval 13151 xpsval 13155 gsumprval 13202 struct2slots2dom 15606 structiedg0val 15608 isomninnlem 15931 trilpolemlt1 15942 iswomninnlem 15950 iswomni0 15952 ismkvnnlem 15953 |
| Copyright terms: Public domain | W3C validator |