Theorem nfrab 2892

Description: A variable not free in a wff remains so in a restricted class abstraction. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 9-Oct-2016.)

Hypotheses

Ref	Expression
nfrab.1	|- F/ x ph
nfrab.2	|- F/_ x A

Assertion

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

Proof of Theorem nfrab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 2714	. 2 |- { y e. A | ph } = { y | ( y e. A /\ ph ) }
2		nftru 1602	. . . 4 |- F/ y T.
3		nfrab.2	. . . . . . . 8 |- F/_ x A
4	3	nfcri 2563	. . . . . . 7 |- F/ x z e. A
5		eleq1 2493	. . . . . . 7 |- ( z = y -> ( z e. A <-> y e. A ) )
6	4, 5	dvelimnf 2030	. . . . . 6 |- ( -. A. x x = y -> F/ x y e. A )
7		nfrab.1	. . . . . . 7 |- F/ x ph
8	7	a1i 11	. . . . . 6 |- ( -. A. x x = y -> F/ x ph )
9	6, 8	nfand 1856	. . . . 5 |- ( -. A. x x = y -> F/ x ( y e. A /\ ph ) )
10	9	adantl 463	. . . 4 |- ( ( T. /\ -. A. x x = y ) -> F/ x ( y e. A /\ ph ) )
11	2, 10	nfabd2 2587	. . 3 |- ( T. -> F/_ x { y | ( y e. A /\ ph ) } )
12	11	trud 1371	. 2 |- F/_ x { y | ( y e. A /\ ph ) }
13	1, 12	nfcxfr 2566	1 |- F/_ x { y e. A | ph }

Syntax hints:   -. wn 3   /\ wa 369   A.wal 1360   T. wtru 1363   F/wnf 1592   e. wcel 1755   {cab 2419   F/_wnfc 2556   {crab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714

This theorem is referenced by:  nfdif  3465  nfin  3545  reusv6OLD  4491  nfse  4682  mpt2xopoveq  6725  nfoi  7716  scottex  8080  elmptrab  19241  iundisjf  25754  nnindf  25911  nfwlim  27605  finminlem  28354  indexa  28468  stoweidlem16  29654  stoweidlem31  29669  stoweidlem34  29672  stoweidlem35  29673  stoweidlem48  29686  stoweidlem51  29689  stoweidlem53  29691  stoweidlem54  29692  stoweidlem57  29695  stoweidlem59  29697  elfvmptrab1  29997  elovmpt2rab  30001  elovmpt2rab1  30002  ovmpt3rab1  30004  elovmpt3rab1  30006  bnj1398  31724  bnj1445  31734  bnj1449  31738