Metamath Proof Explorer

Theorem zfrep4

Description: A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995)

Ref Expression
Hypotheses zfrep4.1 ⊢ x | φ ∈ V
zfrep4.2 ⊢ φ → ∃ z ∀ y ψ → y = z
Assertion zfrep4 ⊢ y | ∃ x φ ∧ ψ ∈ V

Proof

Step Hyp Ref Expression
1 zfrep4.1 ⊢ x | φ ∈ V
2 zfrep4.2 ⊢ φ → ∃ z ∀ y ψ → y = z
3 abid ⊢ x ∈ x | φ ↔ φ
4 3 anbi1i ⊢ x ∈ x | φ ∧ ψ ↔ φ ∧ ψ
5 4 exbii ⊢ ∃ x x ∈ x | φ ∧ ψ ↔ ∃ x φ ∧ ψ
6 5 abbii ⊢ y | ∃ x x ∈ x | φ ∧ ψ = y | ∃ x φ ∧ ψ
7 nfab1 ⊢ Ⅎ _ x x | φ
8 3 2 sylbi ⊢ x ∈ x | φ → ∃ z ∀ y ψ → y = z
9 7 1 8 zfrepclf ⊢ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ x | φ ∧ ψ
10 abeq2 ⊢ z = y | ∃ x x ∈ x | φ ∧ ψ ↔ ∀ y y ∈ z ↔ ∃ x x ∈ x | φ ∧ ψ
11 10 exbii ⊢ ∃ z z = y | ∃ x x ∈ x | φ ∧ ψ ↔ ∃ z ∀ y y ∈ z ↔ ∃ x x ∈ x | φ ∧ ψ
12 9 11 mpbir ⊢ ∃ z z = y | ∃ x x ∈ x | φ ∧ ψ
13 12 issetri ⊢ y | ∃ x x ∈ x | φ ∧ ψ ∈ V
14 6 13 eqeltrri ⊢ y | ∃ x φ ∧ ψ ∈ V