Theorem nfex 1886

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

Syntax hints:   E.wex 1587   F/wnf 1590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591

This theorem is referenced by:  19.12  1888  eeor  1916  eean  1943  eeeanv  1945  cbvex2OLD  1989  nfeu1  2275  moexex  2358  moexexOLD  2359  nfelOLD  2630  ceqsex2  3116  nfopab  4468  nfopab2  4470  cbvopab1  4473  cbvopab1s  4475  axrep2  4516  axrep3  4517  axrep4  4518  copsex2t  4689  copsex2g  4690  mosubopt  4700  euotd  4703  nfco  5116  dfdmf  5144  dfrnf  5189  nfdm  5192  fv3  5815  nfoprab2  6248  nfoprab3  6249  nfoprab  6250  cbvoprab1  6270  cbvoprab2  6271  cbvoprab3  6274  ac6sfi  7670  aceq1  8402  zfcndrep  8896  zfcndinf  8900  nfsum1  13289  nfsum  13290  fsum2dlem  13359  cnvoprab  26201  nfcprod1  27590  nfcprod  27591  fprod2dlem  27658  nfwrecs  27886  pm11.71  29821  stoweidlem57  30023  oprabv  30328  bnj981  32298  bnj1388  32379  bnj1445  32390  bnj1489  32402  bj-axrep2  32667  bj-axrep3  32668  bj-axrep4  32669