Theorem nfex 2004

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

Syntax hints:   E.wex 1659   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905

This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664

This theorem is referenced by:  19.12  2006  eeor  2031  eean  2042  eeeanv  2044  nfeu1  2276  moexex  2337  nfelOLD  2598  ceqsex2  3119  nfopab  4486  nfopab2  4488  cbvopab1  4491  cbvopab1s  4493  axrep2  4535  axrep3  4536  axrep4  4537  copsex2t  4704  copsex2g  4705  mosubopt  4715  euotd  4718  nfco  5016  dfdmf  5044  dfrnf  5089  nfdm  5092  fv3  5891  oprabv  6350  nfoprab2  6352  nfoprab3  6353  nfoprab  6354  cbvoprab1  6374  cbvoprab2  6375  cbvoprab3  6378  nfwrecs  7035  ac6sfi  7818  aceq1  8549  zfcndrep  9040  zfcndinf  9044  nfsum1  13744  nfsum  13745  fsum2dlem  13819  nfcprod1  13952  nfcprod  13953  fprod2dlem  14022  brabgaf  28206  cnvoprab  28302  bnj981  29757  bnj1388  29838  bnj1445  29849  bnj1489  29861  bj-axrep2  31362  bj-axrep3  31363  bj-axrep4  31364  pm11.71  36605  upbdrech  37365  stoweidlem57  37738