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

Theorem nfex 1953
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 1879 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1951 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1628 1  |-  F/ x E. y ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1617   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  19.12  1955  eeor  1981  eean  1992  eeeanv  1994  nfeu1  2296  moexex  2360  nfelOLD  2630  ceqsex2  3144  nfopab  4504  nfopab2  4506  cbvopab1  4509  cbvopab1s  4511  axrep2  4552  axrep3  4553  axrep4  4554  copsex2t  4723  copsex2g  4724  mosubopt  4734  euotd  4737  nfco  5157  dfdmf  5185  dfrnf  5230  nfdm  5233  fv3  5861  oprabv  6318  nfoprab2  6320  nfoprab3  6321  nfoprab  6322  cbvoprab1  6342  cbvoprab2  6343  cbvoprab3  6346  ac6sfi  7756  aceq1  8489  zfcndrep  8981  zfcndinf  8985  nfsum1  13594  nfsum  13595  fsum2dlem  13667  nfcprod1  13799  nfcprod  13800  fprod2dlem  13866  brabgaf  27676  cnvoprab  27777  nfwrecs  29578  pm11.71  31544  upbdrech  31744  stoweidlem57  32078  bnj981  34409  bnj1388  34490  bnj1445  34501  bnj1489  34513  bj-axrep2  34776  bj-axrep3  34777  bj-axrep4  34778
  Copyright terms: Public domain W3C validator