Metamath Proof Explorer

Theorem elrabf

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003)

Ref Expression
Hypotheses elrabf.1 ⊢ Ⅎ _ x A
elrabf.2 ⊢ Ⅎ _ x B
elrabf.3 ⊢ Ⅎ x ψ
elrabf.4 ⊢ x = A → φ ↔ ψ
Assertion elrabf ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ

Proof

Step Hyp Ref Expression
1 elrabf.1 ⊢ Ⅎ _ x A
2 elrabf.2 ⊢ Ⅎ _ x B
3 elrabf.3 ⊢ Ⅎ x ψ
4 elrabf.4 ⊢ x = A → φ ↔ ψ
5 elex ⊢ A ∈ x ∈ B | φ → A ∈ V
6 elex ⊢ A ∈ B → A ∈ V
7 6 adantr ⊢ A ∈ B ∧ ψ → A ∈ V
8 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
9 8 eleq2i ⊢ A ∈ x ∈ B | φ ↔ A ∈ x | x ∈ B ∧ φ
10 1 2 nfel ⊢ Ⅎ x A ∈ B
11 10 3 nfan ⊢ Ⅎ x A ∈ B ∧ ψ
12 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
13 12 4 anbi12d ⊢ x = A → x ∈ B ∧ φ ↔ A ∈ B ∧ ψ
14 1 11 13 elabgf ⊢ A ∈ V → A ∈ x | x ∈ B ∧ φ ↔ A ∈ B ∧ ψ
15 9 14 bitrid ⊢ A ∈ V → A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ
16 5 7 15 pm5.21nii ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ ψ