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

Metamath Proof Explorer

Theorem elrabsf

Description: Membership in a restricted class abstraction, expressed with explicit class substitution. (The variation elrabf has implicit substitution). The hypothesis specifies that x must not be a free variable in B . (Contributed by NM, 30-Sep-2003) (Proof shortened by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypothesis elrabsf.1 ⊢ Ⅎ _ x B
Assertion elrabsf ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 elrabsf.1 ⊢ Ⅎ _ x B
2 dfsbcq ⊢ y = A → [˙y / x]˙ φ ↔ [˙A / x]˙ φ
3 nfcv ⊢ Ⅎ _ y B
4 nfv ⊢ Ⅎ y φ
5 nfsbc1v ⊢ Ⅎ x [˙y / x]˙ φ
6 sbceq1a ⊢ x = y → φ ↔ [˙y / x]˙ φ
7 1 3 4 5 6 cbvrabw ⊢ x ∈ B | φ = y ∈ B | [˙y / x]˙ φ
8 2 7 elrab2 ⊢ A ∈ x ∈ B | φ ↔ A ∈ B ∧ [˙A / x]˙ φ