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

Theorem nfex 1865
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 1778 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1863 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1560 1  |-  F/ x E. y ph
Colors of variables: wff set class
Syntax hints:   E.wex 1550   F/wnf 1553
This theorem is referenced by:  19.12  1869  excomimOLD  1881  eeor  1907  eean  1936  eeeanv  1938  cbvex2  1991  nfeu1  2291  moexex  2350  nfel  2580  ceqsex2  2985  nfopab  4266  nfopab2  4268  cbvopab1  4271  cbvopab1s  4273  axrep2  4315  axrep3  4316  axrep4  4317  copsex2t  4436  copsex2g  4437  mosubopt  4447  euotd  4450  nfco  5031  dfdmf  5057  dfrnf  5101  nfdm  5104  fv3  5737  nfoprab2  6117  nfoprab3  6118  nfoprab  6119  cbvoprab1  6137  cbvoprab2  6138  cbvoprab3  6141  ac6sfi  7344  aceq1  7991  zfcndrep  8482  zfcndinf  8486  nfsum1  12477  nfsum  12478  fsum2dlem  12547  nfcprod1  25229  nfcprod  25230  fprod2dlem  25297  nfwrecs  25526  pm11.71  27565  stoweidlem57  27774  bnj981  29259  bnj1388  29340  bnj1445  29351  bnj1489  29363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator