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

Theorem nfex 1855
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 1770 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1853 . 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  1859  excomimOLD  1870  eeor  1896  eean  1925  eeeanv  1927  cbvex2  2031  nfeu1  2241  moexex  2300  nfel  2524  ceqsex2  2928  nfopab  4207  nfopab2  4209  cbvopab1  4212  cbvopab1s  4214  axrep2  4256  axrep3  4257  axrep4  4258  copsex2t  4377  copsex2g  4378  mosubopt  4388  euotd  4391  nfco  4971  dfdmf  4997  dfrnf  5041  nfdm  5044  fv3  5677  nfoprab2  6056  nfoprab3  6057  nfoprab  6058  cbvoprab1  6076  cbvoprab2  6077  cbvoprab3  6080  ac6sfi  7280  aceq1  7924  zfcndrep  8415  zfcndinf  8419  nfsum1  12404  nfsum  12405  fsum2dlem  12474  nfcprod1  25008  nfcprod  25009  pm11.71  27258  stoweidlem57  27467  bnj981  28652  bnj1388  28733  bnj1445  28744  bnj1489  28756
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator