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

Theorem nfrab 3008
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 2808 . 2  |-  { y  e.  A  |  ph }  =  { y  |  ( y  e.  A  /\  ph ) }
2 nftru 1600 . . . 4  |-  F/ y T.
3 nfrab.2 . . . . . . . 8  |-  F/_ x A
43nfcri 2609 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2526 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 2041 . . . . . 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 1863 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  F/ x
( y  e.  A  /\  ph ) )
109adantl 466 . . . 4  |-  ( ( T.  /\  -.  A. x  x  =  y
)  ->  F/ x
( y  e.  A  /\  ph ) )
112, 10nfabd2 2637 . . 3  |-  ( T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1379 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2614 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369   A.wal 1368   T. wtru 1371   F/wnf 1590    e. wcel 1758   {cab 2439   F/_wnfc 2602   {crab 2803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808
This theorem is referenced by:  nfdif  3588  nfin  3668  reusv6OLD  4614  nfse  4806  mpt2xopoveq  6849  nfoi  7843  scottex  8207  elmptrab  19542  iundisjf  26109  nnindf  26261  nfwlim  27926  finminlem  28684  indexa  28798  stoweidlem16  29982  stoweidlem31  29997  stoweidlem34  30000  stoweidlem35  30001  stoweidlem48  30014  stoweidlem51  30017  stoweidlem53  30019  stoweidlem54  30020  stoweidlem57  30023  stoweidlem59  30025  elfvmptrab1  30325  elovmpt2rab  30329  elovmpt2rab1  30330  ovmpt3rab1  30332  elovmpt3rab1  30334  bnj1398  32380  bnj1445  32390  bnj1449  32394
  Copyright terms: Public domain W3C validator