Theorem nfex 2031

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

Syntax hints:   E.wex 1663   F/wnf 1667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668

This theorem is referenced by:  19.12  2033  eeor  2056  eean  2077  eeeanv  2079  nfeu1  2309  moexex  2370  ceqsex2  3086  nfopab  4468  nfopab2  4470  cbvopab1  4473  cbvopab1s  4475  axrep2  4517  axrep3  4518  axrep4  4519  copsex2t  4688  copsex2g  4689  mosubopt  4699  euotd  4702  nfco  5000  dfdmf  5028  dfrnf  5073  nfdm  5076  fv3  5878  oprabv  6339  nfoprab2  6341  nfoprab3  6342  nfoprab  6343  cbvoprab1  6363  cbvoprab2  6364  cbvoprab3  6367  nfwrecs  7030  ac6sfi  7815  aceq1  8548  zfcndrep  9039  zfcndinf  9043  nfsum1  13756  nfsum  13757  fsum2dlem  13831  nfcprod1  13964  nfcprod  13965  fprod2dlem  14034  brabgaf  28216  cnvoprab  28308  bnj981  29761  bnj1388  29842  bnj1445  29853  bnj1489  29865  bj-axrep2  31404  bj-axrep3  31405  bj-axrep4  31406  pm11.71  36747  upbdrech  37523  stoweidlem57  37918