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

Theorem nfex 1872
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 1807 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1870 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1599 1  |-  F/ x E. y ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1589   F/wnf 1592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593
This theorem is referenced by:  19.12  1874  eeor  1902  eean  1929  eeeanv  1931  cbvex2OLD  1976  nfeu1  2264  moexex  2345  moexexOLD  2346  nfel  2577  ceqsex2  2999  nfopab  4345  nfopab2  4347  cbvopab1  4350  cbvopab1s  4352  axrep2  4393  axrep3  4394  axrep4  4395  copsex2t  4566  copsex2g  4567  mosubopt  4577  euotd  4580  nfco  4992  dfdmf  5020  dfrnf  5065  nfdm  5068  fv3  5691  nfoprab2  6125  nfoprab3  6126  nfoprab  6127  cbvoprab1  6147  cbvoprab2  6148  cbvoprab3  6151  ac6sfi  7544  aceq1  8275  zfcndrep  8769  zfcndinf  8773  nfsum1  13151  nfsum  13152  fsum2dlem  13221  cnvoprab  25847  nfcprod1  27270  nfcprod  27271  fprod2dlem  27338  nfwrecs  27566  pm11.71  29495  stoweidlem57  29698  oprabv  30003  bnj981  31645  bnj1388  31726  bnj1445  31737  bnj1489  31749  bj-axrep2  31930  bj-axrep3  31931  bj-axrep4  31932
  Copyright terms: Public domain W3C validator