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

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

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