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

Theorem nfex 1895
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 1822 . . 3  |-  ( ph  ->  A. x ph )
32hbex 1893 . 2  |-  ( E. y ph  ->  A. x E. y ph )
43nfi 1606 1  |-  F/ x E. y ph
Colors of variables: wff setvar class
Syntax hints:   E.wex 1596   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  19.12  1897  eeor  1925  eean  1956  eeeanv  1958  cbvex2OLD  2002  nfeu1  2288  moexex  2371  moexexOLD  2372  nfelOLD  2643  ceqsex2  3156  nfopab  4518  nfopab2  4520  cbvopab1  4523  cbvopab1s  4525  axrep2  4566  axrep3  4567  axrep4  4568  copsex2t  4740  copsex2g  4741  mosubopt  4751  euotd  4754  nfco  5174  dfdmf  5202  dfrnf  5247  nfdm  5250  fv3  5885  oprabv  6340  nfoprab2  6342  nfoprab3  6343  nfoprab  6344  cbvoprab1  6364  cbvoprab2  6365  cbvoprab3  6368  ac6sfi  7776  aceq1  8510  zfcndrep  9004  zfcndinf  9008  nfsum1  13492  nfsum  13493  fsum2dlem  13565  cnvoprab  27369  nfcprod1  28969  nfcprod  28970  fprod2dlem  29037  nfwrecs  29265  pm11.71  31205  upbdrech  31405  stoweidlem57  31680  bnj981  33488  bnj1388  33569  bnj1445  33580  bnj1489  33592  bj-axrep2  33857  bj-axrep3  33858  bj-axrep4  33859
  Copyright terms: Public domain W3C validator