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 
|- F/_ x B
Assertion elrabsf 
|- ( A e. { x e. B | ph } <-> ( A e. B /\ [. A / x ]. ph ) )

Proof

Step Hyp Ref Expression
1 elrabsf.1 
 |-  F/_ x B
2 dfsbcq 
 |-  ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) )
3 nfcv 
 |-  F/_ y B
4 nfv 
 |-  F/ y ph
5 nfsbc1v 
 |-  F/ x [. y / x ]. ph
6 sbceq1a 
 |-  ( x = y -> ( ph <-> [. y / x ]. ph ) )
7 1 3 4 5 6 cbvrabw 
 |-  { x e. B | ph } = { y e. B | [. y / x ]. ph }
8 2 7 elrab2 
 |-  ( A e. { x e. B | ph } <-> ( A e. B /\ [. A / x ]. ph ) )