| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The Axiom of Pairing of
Zermelo-Fraenkel set theory. Axiom 2 of
[TakeutiZaring] p. 15. In some
textbooks this is stated as a separate
axiom; here we show it is redundant since it can be derived from the
other axioms.
This theorem should not be referenced by any proof other than axpr 3338. Instead, use zfpair2 3340 below so that the uses of the Axiom of Pairing can be more easily identified. |
| Ref | Expression |
|---|---|
| zfpair |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfpr2 2883 |
. 2
| |
| 2 | 19.43 1278 |
. . . . 5
| |
| 3 | prlem2 847 |
. . . . . 6
| |
| 4 | 3 | exbii 1236 |
. . . . 5
|
| 5 | 19.41v 1523 |
. . . . . . 7
| |
| 6 | 0ex 3261 |
. . . . . . . 8
| |
| 7 | 6 | isseti 2130 |
. . . . . . 7
|
| 8 | 5, 7 | mpbiran 795 |
. . . . . 6
|
| 9 | 19.41v 1523 |
. . . . . . 7
| |
| 10 | p0ex 3310 |
. . . . . . . 8
| |
| 11 | 10 | isseti 2130 |
. . . . . . 7
|
| 12 | 9, 11 | mpbiran 795 |
. . . . . 6
|
| 13 | 8, 12 | orbi12i 275 |
. . . . 5
|
| 14 | 2, 4, 13 | 3bitr3ri 198 |
. . . 4
|
| 15 | 14 | abbii 1843 |
. . 3
|
| 16 | dfpr2 2883 |
. . . . 5
| |
| 17 | pp0ex 3311 |
. . . . 5
| |
| 18 | 16, 17 | eqeltrri 1805 |
. . . 4
|
| 19 | equequ2 1333 |
. . . . . . . 8
| |
| 20 | 0inp0 3290 |
. . . . . . . 8
| |
| 21 | 19, 20 | prlem1 845 |
. . . . . . 7
|
| 22 | 21 | 19.21adv 1504 |
. . . . . 6
|
| 23 | 22 | a4imev 1488 |
. . . . 5
|
| 24 | equequ2 1333 |
. . . . . . . . 9
| |
| 25 | 20 | con2i 112 |
. . . . . . . . 9
|
| 26 | 24, 25 | prlem1 845 |
. . . . . . . 8
|
| 27 | orcom 264 |
. . . . . . . 8
| |
| 28 | 26, 27 | syl7ib 232 |
. . . . . . 7
|
| 29 | 28 | 19.21adv 1504 |
. . . . . 6
|
| 30 | 29 | a4imev 1488 |
. . . . 5
|
| 31 | 23, 30 | jaoi 366 |
. . . 4
|
| 32 | 18, 31 | zfrep4 3251 |
. . 3
|
| 33 | 15, 32 | eqeltri 1804 |
. 2
|
| 34 | 1, 33 | eqeltri 1804 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: axpr 3338 dfdir2 14365 latdir 14369 clatlat 16650 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1142 ax-gen 1143 ax-8 1144 ax-9 1145 ax-10 1146 ax-11 1147 ax-12 1148 ax-14 1150 ax-17 1155 ax-4 1157 ax-5o 1159 ax-6o 1162 ax-9o 1319 ax-10o 1338 ax-16 1418 ax-11o 1426 ax-ext 1702 ax-rep 3243 ax-sep 3253 ax-nul 3260 ax-pow 3296 |
| This theorem depends on definitions: df-bi 163 df-or 240 df-an 241 df-ex 1165 df-sb 1374 df-clab 1709 df-cleq 1714 df-clel 1717 df-ne 1856 df-v 2127 df-dif 2430 df-un 2433 df-in 2436 df-ss 2438 df-nul 2702 df-pw 2859 df-sn 2873 df-pr 2874 |