This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zfrepclf

Description: An inference based on the Axiom of Replacement. Typically, ph defines a function from x to y . (Contributed by NM, 26-Nov-1995)

Ref Expression
Hypotheses zfrepclf.1 ⊢ Ⅎ _ x A
zfrepclf.2 ⊢ A ∈ V
zfrepclf.3 ⊢ x ∈ A → ∃ z ∀ y φ → y = z
Assertion zfrepclf ⊢ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ A ∧ φ

Proof

Step Hyp Ref Expression
1 zfrepclf.1 ⊢ Ⅎ _ x A
2 zfrepclf.2 ⊢ A ∈ V
3 zfrepclf.3 ⊢ x ∈ A → ∃ z ∀ y φ → y = z
4 1 nfeq2 ⊢ Ⅎ x v = A
5 eleq2 ⊢ v = A → x ∈ v ↔ x ∈ A
6 5 3 biimtrdi ⊢ v = A → x ∈ v → ∃ z ∀ y φ → y = z
7 4 6 alrimi ⊢ v = A → ∀ x x ∈ v → ∃ z ∀ y φ → y = z
8 nfv ⊢ Ⅎ z φ
9 8 axrep5 ⊢ ∀ x x ∈ v → ∃ z ∀ y φ → y = z → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ v ∧ φ
10 7 9 syl ⊢ v = A → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ v ∧ φ
11 5 anbi1d ⊢ v = A → x ∈ v ∧ φ ↔ x ∈ A ∧ φ
12 4 11 exbid ⊢ v = A → ∃ x x ∈ v ∧ φ ↔ ∃ x x ∈ A ∧ φ
13 12 bibi2d ⊢ v = A → y ∈ z ↔ ∃ x x ∈ v ∧ φ ↔ y ∈ z ↔ ∃ x x ∈ A ∧ φ
14 13 albidv ⊢ v = A → ∀ y y ∈ z ↔ ∃ x x ∈ v ∧ φ ↔ ∀ y y ∈ z ↔ ∃ x x ∈ A ∧ φ
15 14 exbidv ⊢ v = A → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ v ∧ φ ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ A ∧ φ
16 10 15 mpbid ⊢ v = A → ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ A ∧ φ
17 2 16 vtocle ⊢ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ A ∧ φ