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

Metamath Proof Explorer

Theorem rabeqf

Description: Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004)

Ref Expression
Hypotheses rabeqf.1 ⊢ Ⅎ _ x A
rabeqf.2 ⊢ Ⅎ _ x B
Assertion rabeqf ⊢ A = B → x ∈ A | φ = x ∈ B | φ

Proof

Step Hyp Ref Expression
1 rabeqf.1 ⊢ Ⅎ _ x A
2 rabeqf.2 ⊢ Ⅎ _ x B
3 1 2 nfeq ⊢ Ⅎ x A = B
4 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
5 4 anbi1d ⊢ A = B → x ∈ A ∧ φ ↔ x ∈ B ∧ φ
6 3 5 abbid ⊢ A = B → x | x ∈ A ∧ φ = x | x ∈ B ∧ φ
7 df-rab ⊢ x ∈ A | φ = x | x ∈ A ∧ φ
8 df-rab ⊢ x ∈ B | φ = x | x ∈ B ∧ φ
9 6 7 8 3eqtr4g ⊢ A = B → x ∈ A | φ = x ∈ B | φ