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

Theorem nfrab 3007
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 2780 . 2  |-  { y  e.  A  |  ph }  =  { y  |  ( y  e.  A  /\  ph ) }
2 nftru 1671 . . . 4  |-  F/ y T.
3 nfrab.2 . . . . . . . 8  |-  F/_ x A
43nfcri 2573 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2495 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 2140 . . . . . 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 1985 . . . . 5  |-  ( -. 
A. x  x  =  y  ->  F/ x
( y  e.  A  /\  ph ) )
109adantl 467 . . . 4  |-  ( ( T.  /\  -.  A. x  x  =  y
)  ->  F/ x
( y  e.  A  /\  ph ) )
112, 10nfabd2 2601 . . 3  |-  ( T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1446 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2578 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 370   A.wal 1435   T. wtru 1438   F/wnf 1661    e. wcel 1872   {cab 2407   F/_wnfc 2566   {crab 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rab 2780
This theorem is referenced by:  nfdif  3586  nfin  3669  nfse  4828  elfvmptrab1  5986  elovmpt2rab  6529  elovmpt2rab1  6530  ovmpt3rab1  6539  elovmpt3rab1  6541  mpt2xopoveq  6976  nfoi  8038  scottex  8364  elmptrab  20840  iundisjf  28201  nnindf  28389  bnj1398  29851  bnj1445  29861  bnj1449  29865  nfwlim  30512  finminlem  30979  poimirlem26  31930  poimirlem27  31931  indexa  32024  binomcxplemdvbinom  36672  binomcxplemdvsum  36674  binomcxplemnotnn0  36675  dvnprodlem1  37761  stoweidlem16  37816  stoweidlem31  37832  stoweidlem34  37835  stoweidlem35  37836  stoweidlem48  37849  stoweidlem51  37852  stoweidlem53  37854  stoweidlem54  37855  stoweidlem57  37858  stoweidlem59  37860  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem48  37958  fourierdlem51  37961  etransclem32  38071  ovncvrrp  38290
  Copyright terms: Public domain W3C validator