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

Metamath Proof Explorer

Theorem rabxfrd

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, 16-Jan-2012)

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

Proof

Step Hyp Ref Expression
1 rabxfrd.1 ⊢ Ⅎ _ y B
2 rabxfrd.2 ⊢ Ⅎ _ y C
3 rabxfrd.3 ⊢ φ ∧ y ∈ D → A ∈ D
4 rabxfrd.4 ⊢ x = A → ψ ↔ χ
5 rabxfrd.5 ⊢ y = B → A = C
6 3 ex ⊢ φ → y ∈ D → A ∈ D
7 ibibr ⊢ y ∈ D → A ∈ D ↔ y ∈ D → A ∈ D ↔ y ∈ D
8 6 7 sylib ⊢ φ → y ∈ D → A ∈ D ↔ y ∈ D
9 8 imp ⊢ φ ∧ y ∈ D → A ∈ D ↔ y ∈ D
10 9 anbi1d ⊢ φ ∧ y ∈ D → A ∈ D ∧ χ ↔ y ∈ D ∧ χ
11 4 elrab ⊢ A ∈ x ∈ D | ψ ↔ A ∈ D ∧ χ
12 rabid ⊢ y ∈ y ∈ D | χ ↔ y ∈ D ∧ χ
13 10 11 12 3bitr4g ⊢ φ ∧ y ∈ D → A ∈ x ∈ D | ψ ↔ y ∈ y ∈ D | χ
14 13 rabbidva ⊢ φ → y ∈ D | A ∈ x ∈ D | ψ = y ∈ D | y ∈ y ∈ D | χ
15 14 eleq2d ⊢ φ → B ∈ y ∈ D | A ∈ x ∈ D | ψ ↔ B ∈ y ∈ D | y ∈ y ∈ D | χ
16 nfcv ⊢ Ⅎ _ y D
17 2 nfel1 ⊢ Ⅎ y C ∈ x ∈ D | ψ
18 5 eleq1d ⊢ y = B → A ∈ x ∈ D | ψ ↔ C ∈ x ∈ D | ψ
19 1 16 17 18 elrabf ⊢ B ∈ y ∈ D | A ∈ x ∈ D | ψ ↔ B ∈ D ∧ C ∈ x ∈ D | ψ
20 nfrab1 ⊢ Ⅎ _ y y ∈ D | χ
21 1 20 nfel ⊢ Ⅎ y B ∈ y ∈ D | χ
22 eleq1 ⊢ y = B → y ∈ y ∈ D | χ ↔ B ∈ y ∈ D | χ
23 1 16 21 22 elrabf ⊢ B ∈ y ∈ D | y ∈ y ∈ D | χ ↔ B ∈ D ∧ B ∈ y ∈ D | χ
24 15 19 23 3bitr3g ⊢ φ → B ∈ D ∧ C ∈ x ∈ D | ψ ↔ B ∈ D ∧ B ∈ y ∈ D | χ
25 pm5.32 ⊢ B ∈ D → C ∈ x ∈ D | ψ ↔ B ∈ y ∈ D | χ ↔ B ∈ D ∧ C ∈ x ∈ D | ψ ↔ B ∈ D ∧ B ∈ y ∈ D | χ
26 24 25 sylibr ⊢ φ → B ∈ D → C ∈ x ∈ D | ψ ↔ B ∈ y ∈ D | χ
27 26 imp ⊢ φ ∧ B ∈ D → C ∈ x ∈ D | ψ ↔ B ∈ y ∈ D | χ