MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfrab Structured version   Unicode version

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.
StepHypRef 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
43nfcri 2563 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2493 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 2030 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  F/ x  y  e.  A )
7 nfrab.1 . . . . . . 7  |-  F/ x ph
87a1i 11 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  F/ x ph )
96, 8nfand 1856 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  F/ x
( y  e.  A  /\  ph ) )
109adantl 463 . . . 4  |-  ( ( T.  /\  -.  A. x  x  =  y
)  ->  F/ x
( y  e.  A  /\  ph ) )
112, 10nfabd2 2587 . . 3  |-  ( T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1371 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2566 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator