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

Theorem nfrab 2881
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 2706 . 2  |-  { y  e.  A  |  ph }  =  { y  |  ( y  e.  A  /\  ph ) }
2 nftru 1563 . . . 4  |-  F/ y  T.
3 nfrab.2 . . . . . . . 8  |-  F/_ x A
43nfcri 2565 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2495 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 2071 . . . . . 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 1843 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  F/ x
( y  e.  A  /\  ph ) )
109adantl 453 . . . 4  |-  ( (  T.  /\  -.  A. x  x  =  y
)  ->  F/ x
( y  e.  A  /\  ph ) )
112, 10nfabd2 2589 . . 3  |-  (  T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1332 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2568 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 359    T. wtru 1325   A.wal 1549   F/wnf 1553    e. wcel 1725   {cab 2421   F/_wnfc 2558   {crab 2701
This theorem is referenced by:  nfdif  3460  nfin  3539  nfse  4549  reusv6OLD  4726  mpt2xopoveq  6462  nfoi  7475  scottex  7801  elmptrab  17851  iundisjf  24021  nfwlim  25565  finminlem  26302  indexa  26416  stoweidlem16  27722  stoweidlem31  27737  stoweidlem34  27740  stoweidlem35  27741  stoweidlem48  27754  stoweidlem51  27757  stoweidlem53  27759  stoweidlem54  27760  stoweidlem57  27763  stoweidlem59  27765  bnj1398  29330  bnj1445  29340  bnj1449  29344
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706
  Copyright terms: Public domain W3C validator