Theorem nfex 2050

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 1972	. . 3 |- ( ph -> A. x ph )
3	2	hbex 2048	. 2 |- ( E. y ph -> A. x E. y ph )
4	3	nfi 1682	1 |- F/ x E. y ph

Syntax hints:   E.wex 1671   F/wnf 1675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950

This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676

This theorem is referenced by:  19.12  2052  eeor  2075  eean  2092  eeeanv  2094  nfeu1  2329  moexex  2390  ceqsex2  3072  nfopab  4461  nfopab2  4463  cbvopab1  4466  cbvopab1s  4468  axrep2  4510  axrep3  4511  axrep4  4512  copsex2t  4688  copsex2g  4689  mosubopt  4699  euotd  4702  nfco  5005  dfdmf  5033  dfrnf  5079  nfdm  5082  fv3  5892  oprabv  6358  nfoprab2  6360  nfoprab3  6361  nfoprab  6362  cbvoprab1  6382  cbvoprab2  6383  cbvoprab3  6386  nfwrecs  7048  ac6sfi  7833  aceq1  8566  zfcndrep  9057  zfcndinf  9061  nfsum1  13833  nfsum  13834  fsum2dlem  13908  nfcprod1  14041  nfcprod  14042  fprod2dlem  14111  brabgaf  28292  cnvoprab  28383  bnj981  29833  bnj1388  29914  bnj1445  29925  bnj1489  29937  bj-axrep2  31470  bj-axrep3  31471  bj-axrep4  31472  pm11.71  36817  upbdrech  37611  stoweidlem57  38030