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

Theorem nfex 1861
Description: If  x is not free in  ph, it is not free in  E. y ph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypothesis
Ref Expression
nfal.1  |-  F/ x ph
Assertion
Ref Expression
nfex  |-  F/ x E. y ph

Proof of Theorem nfex
StepHypRef Expression
1 nfal.1 . . . 4  |-  F/ x ph
21nfri 1774 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1859 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1557 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   E.wex 1547   F/wnf 1550
This theorem is referenced by:  19.12  1865  excomimOLD  1877  eeor  1903  eean  1932  eeeanv  1934  cbvex2  2055  nfeu1  2264  moexex  2323  nfel  2548  ceqsex2  2952  nfopab  4233  nfopab2  4235  cbvopab1  4238  cbvopab1s  4240  axrep2  4282  axrep3  4283  axrep4  4284  copsex2t  4403  copsex2g  4404  mosubopt  4414  euotd  4417  nfco  4997  dfdmf  5023  dfrnf  5067  nfdm  5070  fv3  5703  nfoprab2  6083  nfoprab3  6084  nfoprab  6085  cbvoprab1  6103  cbvoprab2  6104  cbvoprab3  6107  ac6sfi  7310  aceq1  7954  zfcndrep  8445  zfcndinf  8449  nfsum1  12439  nfsum  12440  fsum2dlem  12509  nfcprod1  25189  nfcprod  25190  fprod2dlem  25257  pm11.71  27464  stoweidlem57  27673  bnj981  29027  bnj1388  29108  bnj1445  29119  bnj1489  29131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator