| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Axiom of Replacement ax-rep 3628, reproved from conditionless ZFC axioms. |
| Ref | Expression |
|---|---|
| zfcndrep |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbe1 1681 |
. . . . . 6
| |
| 2 | ax-17 1634 |
. . . . . . . 8
| |
| 3 | ax-17 1634 |
. . . . . . . . . 10
| |
| 4 | hba1 1668 |
. . . . . . . . . 10
| |
| 5 | 3, 4 | hban 1674 |
. . . . . . . . 9
|
| 6 | 5 | hbex 1671 |
. . . . . . . 8
|
| 7 | 2, 6 | hbbi 1675 |
. . . . . . 7
|
| 8 | 7 | hbal 1670 |
. . . . . 6
|
| 9 | 1, 8 | hbim 1672 |
. . . . 5
|
| 10 | 9 | hbex 1671 |
. . . 4
|
| 11 | elequ2 1807 |
. . . . . . . . . 10
| |
| 12 | 11 | anbi1d 815 |
. . . . . . . . 9
|
| 13 | 12 | exbidv 1955 |
. . . . . . . 8
|
| 14 | 13 | bibi2d 382 |
. . . . . . 7
|
| 15 | 14 | albidv 1954 |
. . . . . 6
|
| 16 | 15 | imbi2d 380 |
. . . . 5
|
| 17 | 16 | exbidv 1955 |
. . . 4
|
| 18 | axrepnd 6541 |
. . . . 5
| |
| 19 | 2 | 19.3 1696 |
. . . . . . . . 9
|
| 20 | ax-17 1634 |
. . . . . . . . . . . 12
| |
| 21 | 20 | 19.3 1696 |
. . . . . . . . . . 11
|
| 22 | 21 | anbi1i 805 |
. . . . . . . . . 10
|
| 23 | 22 | exbii 1716 |
. . . . . . . . 9
|
| 24 | 19, 23 | bibi12i 379 |
. . . . . . . 8
|
| 25 | 24 | albii 1664 |
. . . . . . 7
|
| 26 | 25 | imbi2i 373 |
. . . . . 6
|
| 27 | 26 | exbii 1716 |
. . . . 5
|
| 28 | 18, 27 | mpbi 254 |
. . . 4
|
| 29 | 10, 17, 28 | chvar 1839 |
. . 3
|
| 30 | 29 | 19.35i 1742 |
. 2
|
| 31 | ax-17 1634 |
. . . . 5
| |
| 32 | hbe1 1681 |
. . . . 5
| |
| 33 | 31, 32 | hbbi 1675 |
. . . 4
|
| 34 | 33 | hbal 1670 |
. . 3
|
| 35 | elequ2 1807 |
. . . . 5
| |
| 36 | hba1 1668 |
. . . . . . . . 9
| |
| 37 | 36 | 19.3 1696 |
. . . . . . . 8
|
| 38 | 37 | anbi2i 804 |
. . . . . . 7
|
| 39 | 38 | exbii 1716 |
. . . . . 6
|
| 40 | 39 | a1i 8 |
. . . . 5
|
| 41 | 35, 40 | bibi12d 385 |
. . . 4
|
| 42 | 41 | albidv 1954 |
. . 3
|
| 43 | 8, 34, 42 | cbvex 1838 |
. 2
|
| 44 | 30, 43 | sylib 263 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1621 ax-gen 1622 ax-8 1623 ax-9 1624 ax-10 1625 ax-11 1626 ax-12 1627 ax-13 1628 ax-14 1629 ax-17 1634 ax-4 1637 ax-5o 1639 ax-6o 1642 ax-9o 1792 ax-10o 1810 ax-16 1883 ax-11o 1893 ax-15 2044 ax-ext 2152 ax-rep 3628 ax-sep 3638 ax-nul 3645 ax-pow 3681 ax-reg 5972 |
| This theorem depends on definitions: df-bi 232 df-or 434 df-an 435 df-ex 1645 df-sb 1845 df-clab 2158 df-cleq 2163 df-clel 2166 df-ne 2297 df-ral 2389 df-rex 2390 df-v 2571 df-dif 2862 df-in 2866 df-ss 2868 df-nul 3115 df-pw 3261 df-sn 3274 |