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

Theorem nfrab 2984
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 2758 . 2  |-  { y  e.  A  |  ph }  =  { y  |  ( y  e.  A  /\  ph ) }
2 nftru 1688 . . . 4  |-  F/ y T.
3 nfrab.2 . . . . . . . 8  |-  F/_ x A
43nfcri 2597 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2528 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 2184 . . . . . 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 2019 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  F/ x
( y  e.  A  /\  ph ) )
109adantl 472 . . . 4  |-  ( ( T.  /\  -.  A. x  x  =  y
)  ->  F/ x
( y  e.  A  /\  ph ) )
112, 10nfabd2 2622 . . 3  |-  ( T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1464 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2601 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 375   A.wal 1453   T. wtru 1456   F/wnf 1678    e. wcel 1898   {cab 2448   F/_wnfc 2590   {crab 2753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758
This theorem is referenced by:  nfdif  3566  nfin  3651  nfse  4831  elfvmptrab1  5998  elovmpt2rab  6547  elovmpt2rab1  6548  ovmpt3rab1  6557  elovmpt3rab1  6559  mpt2xopoveq  6997  nfoi  8060  scottex  8387  elmptrab  20897  iundisjf  28253  nnindf  28434  bnj1398  29893  bnj1445  29903  bnj1449  29907  nfwlim  30555  finminlem  31024  poimirlem26  32012  poimirlem27  32013  indexa  32106  binomcxplemdvbinom  36747  binomcxplemdvsum  36749  binomcxplemnotnn0  36750  dvnprodlem1  37907  stoweidlem16  37977  stoweidlem31  37993  stoweidlem34  37996  stoweidlem35  37997  stoweidlem48  38010  stoweidlem51  38013  stoweidlem53  38015  stoweidlem54  38016  stoweidlem57  38019  stoweidlem59  38021  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem48  38119  fourierdlem51  38122  etransclem32  38232  ovncvrrp  38493
  Copyright terms: Public domain W3C validator