Metamath Proof Explorer

Theorem rabxfr

Description: Membership in a restricted class abstraction after substituting an expression A (containing y ) for x in the formula defining the class abstraction. (Contributed by NM, 10-Jun-2005)

Ref Expression
Hypotheses rabxfr.1 ⊢ Ⅎ _ y B
rabxfr.2 ⊢ Ⅎ _ y C
rabxfr.3 ⊢ y ∈ D → A ∈ D
rabxfr.4 ⊢ x = A → φ ↔ ψ
rabxfr.5 ⊢ y = B → A = C
Assertion rabxfr ⊢ B ∈ D → C ∈ x ∈ D | φ ↔ B ∈ y ∈ D | ψ

Proof

Step Hyp Ref Expression
1 rabxfr.1 ⊢ Ⅎ _ y B
2 rabxfr.2 ⊢ Ⅎ _ y C
3 rabxfr.3 ⊢ y ∈ D → A ∈ D
4 rabxfr.4 ⊢ x = A → φ ↔ ψ
5 rabxfr.5 ⊢ y = B → A = C
6 tru ⊢ ⊤
7 3 adantl ⊢ ⊤ ∧ y ∈ D → A ∈ D
8 1 2 7 4 5 rabxfrd ⊢ ⊤ ∧ B ∈ D → C ∈ x ∈ D | φ ↔ B ∈ y ∈ D | ψ
9 6 8 mpan ⊢ B ∈ D → C ∈ x ∈ D | φ ↔ B ∈ y ∈ D | ψ