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

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 |- F/ x ph
2	1	nfri 1807	. . 3 |- ( ph -> A. x ph )
3	2	hbex 1870	. 2 |- ( E. y ph -> A. x E. y ph )
4	3	nfi 1599	1 |- F/ x E. y ph

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