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

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

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