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

Theorem nfrab 3048
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 2826 . 2  |-  { y  e.  A  |  ph }  =  { y  |  ( y  e.  A  /\  ph ) }
2 nftru 1609 . . . 4  |-  F/ y T.
3 nfrab.2 . . . . . . . 8  |-  F/_ x A
43nfcri 2622 . . . . . . 7  |-  F/ x  z  e.  A
5 eleq1 2539 . . . . . . 7  |-  ( z  =  y  ->  (
z  e.  A  <->  y  e.  A ) )
64, 5dvelimnf 2054 . . . . . 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 1872 . . . . 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 2650 . . 3  |-  ( T. 
->  F/_ x { y  |  ( y  e.  A  /\  ph ) } )
1211trud 1388 . 2  |-  F/_ x { y  |  ( y  e.  A  /\  ph ) }
131, 12nfcxfr 2627 1  |-  F/_ x { y  e.  A  |  ph }
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    /\ wa 369   A.wal 1377   T. wtru 1380   F/wnf 1599    e. wcel 1767   {cab 2452   F/_wnfc 2615   {crab 2821
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826
This theorem is referenced by:  nfdif  3630  nfin  3710  reusv6OLD  4664  nfse  4860  elfvmptrab1  5977  elovmpt2rab  6516  elovmpt2rab1  6517  ovmpt3rab1  6529  elovmpt3rab1  6531  mpt2xopoveq  6959  nfoi  7951  scottex  8315  elmptrab  20196  iundisjf  27271  nnindf  27434  nfwlim  29305  finminlem  30063  indexa  30151  stoweidlem16  31639  stoweidlem31  31654  stoweidlem34  31657  stoweidlem35  31658  stoweidlem48  31671  stoweidlem51  31674  stoweidlem53  31676  stoweidlem54  31677  stoweidlem57  31680  stoweidlem59  31682  fourierdlem31  31761  fourierdlem48  31778  fourierdlem51  31781  bnj1398  33570  bnj1445  33580  bnj1449  33584
  Copyright terms: Public domain W3C validator