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

Theorem nfrab 2734
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 2565 . 2  |-  { y  e.  A  |  ph }  =  { y  |  ( y  e.  A  /\  ph ) }
2 nftru 1544 . . . 4  |-  F/ y  T.
3 nfrab.2 . . . . . . . 8  |-  F/_ x A
43nfcri 2426 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2356 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 1970 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  F/ x  y  e.  A )
7 nfrab.1 . . . . . . 7  |-  F/ x ph
87a1i 10 . . . . . 6  |-  ( -. 
A. x  x  =  y  ->  F/ x ph )
96, 8nfand 1775 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  F/ x
( y  e.  A  /\  ph ) )
109adantl 452 . . . 4  |-  ( (  T.  /\  -.  A. x  x  =  y
)  ->  F/ x
( y  e.  A  /\  ph ) )
112, 10nfabd2 2450 . . 3  |-  (  T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1314 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2429 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 358    T. wtru 1307   A.wal 1530   F/wnf 1534    = wceq 1632    e. wcel 1696   {cab 2282   F/_wnfc 2419   {crab 2560
This theorem is referenced by:  nfdif  3310  nfin  3388  nfse  4384  reusv6OLD  4561  nfoi  7245  scottex  7571  elmptrab  17538  iundisjf  23380  finminlem  26334  indexa  26515  stoweidlem16  27868  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem48  27900  stoweidlem51  27903  stoweidlem53  27905  stoweidlem54  27906  stoweidlem57  27909  stoweidlem59  27911  mpt2xopoveq  28201  bnj1398  29380  bnj1445  29390  bnj1449  29394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565
  Copyright terms: Public domain W3C validator