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

Metamath Proof Explorer

Theorem nfrab

Description: A variable not free in a wff remains so in a restricted class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfrabw when possible. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfrab.1 
|- F/ x ph
nfrab.2 
|- F/_ x A
Assertion nfrab 
|- F/_ x { y e. A | ph }

Proof

Step Hyp Ref Expression
1 nfrab.1 
 |-  F/ x ph
2 nfrab.2 
 |-  F/_ x A
3 df-rab 
 |-  { y e. A | ph } = { y | ( y e. A /\ ph ) }
4 nftru 
 |-  F/ y T.
5 2 nfcri 
 |-  F/ x z e. A
6 eleq1w 
 |-  ( z = y -> ( z e. A <-> y e. A ) )
7 5 6 dvelimnf 
 |-  ( -. A. x x = y -> F/ x y e. A )
8 1 a1i 
 |-  ( -. A. x x = y -> F/ x ph )
9 7 8 nfand 
 |-  ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10 9 adantl 
 |-  ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11 4 10 nfabd2 
 |-  ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12 11 mptru 
 |-  F/_ x { y | ( y e. A /\ ph ) }
13 3 12 nfcxfr 
 |-  F/_ x { y e. A | ph }