Metamath Proof Explorer

Theorem axrep1

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet https://us.metamath.org/mmsolitaire/mms.html . Equivalence is shown via the path ax-rep -> axrep1 -> axrep2 -> axrepnd -> zfcndrep = ax-rep . (Contributed by NM, 19-Nov-2005) (Proof shortened by Mario Carneiro, 17-Nov-2016) Remove dependency on ax-13 . (Revised by BJ, 31-May-2019)

Ref Expression
Assertion axrep1 ⊢∃x∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧φ

Proof

Step Hyp Ref Expression
1 elequ2 ⊢w=y→x∈w↔x∈y
2 1 anbi1d ⊢w=y→x∈w∧φ↔x∈y∧φ
3 2 exbidv ⊢w=y→∃xx∈w∧φ↔∃xx∈y∧φ
4 3 bibi2d ⊢w=y→z∈x↔∃xx∈w∧φ↔z∈x↔∃xx∈y∧φ
5 4 albidv ⊢w=y→∀zz∈x↔∃xx∈w∧φ↔∀zz∈x↔∃xx∈y∧φ
6 5 exbidv ⊢w=y→∃x∀zz∈x↔∃xx∈w∧φ↔∃x∀zz∈x↔∃xx∈y∧φ
7 6 imbi2d ⊢w=y→∀x∃y∀zφ→z=y→∃x∀zz∈x↔∃xx∈w∧φ↔∀x∃y∀zφ→z=y→∃x∀zz∈x↔∃xx∈y∧φ
8 ax-rep ⊢∀x∃y∀z∀yφ→z=y→∃y∀zz∈y↔∃xx∈w∧∀yφ
9 19.3v ⊢∀yφ↔φ
10 9 imbi1i ⊢∀yφ→z=y↔φ→z=y
11 10 albii ⊢∀z∀yφ→z=y↔∀zφ→z=y
12 11 exbii ⊢∃y∀z∀yφ→z=y↔∃y∀zφ→z=y
13 12 albii ⊢∀x∃y∀z∀yφ→z=y↔∀x∃y∀zφ→z=y
14 nfv ⊢Ⅎxz∈y
15 nfe1 ⊢Ⅎx∃xx∈w∧∀yφ
16 14 15 nfbi ⊢Ⅎxz∈y↔∃xx∈w∧∀yφ
17 16 nfal ⊢Ⅎx∀zz∈y↔∃xx∈w∧∀yφ
18 nfv ⊢Ⅎy∀zz∈x↔∃xx∈w∧φ
19 elequ2 ⊢y=x→z∈y↔z∈x
20 9 anbi2i ⊢x∈w∧∀yφ↔x∈w∧φ
21 20 exbii ⊢∃xx∈w∧∀yφ↔∃xx∈w∧φ
22 21 a1i ⊢y=x→∃xx∈w∧∀yφ↔∃xx∈w∧φ
23 19 22 bibi12d ⊢y=x→z∈y↔∃xx∈w∧∀yφ↔z∈x↔∃xx∈w∧φ
24 23 albidv ⊢y=x→∀zz∈y↔∃xx∈w∧∀yφ↔∀zz∈x↔∃xx∈w∧φ
25 17 18 24 cbvexv1 ⊢∃y∀zz∈y↔∃xx∈w∧∀yφ↔∃x∀zz∈x↔∃xx∈w∧φ
26 8 13 25 3imtr3i ⊢∀x∃y∀zφ→z=y→∃x∀zz∈x↔∃xx∈w∧φ
27 7 26 chvarvv ⊢∀x∃y∀zφ→z=y→∃x∀zz∈x↔∃xx∈y∧φ
28 27 19.35ri ⊢∃x∃y∀zφ→z=y→∀zz∈x↔∃xx∈y∧φ