Theorem nfex 1651

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
nfex.1	|- F/ x ph

Assertion

Ref	Expression
nfex	|- F/ x E. y ph

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		nfex.1	. . . 4 |- F/ x ph
2	1	nfri 1533	. . 3 |- ( ph -> A. x ph )
3	2	hbex 1650	. 2 |- ( E. y ph -> A. x E. y ph )
4	3	nfi 1476	1 |- F/ x E. y ph

Syntax hints:   F/wnf 1474   E.wex 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524

This theorem depends on definitions:  df-bi 117  df-nf 1475

This theorem is referenced by:  eeor  1709  cbvexv1  1766  cbvex2  1937  eean  1950  nfsbv  1966  nfeu1  2056  nfeuv  2063  nfel  2348  ceqsex2  2804  nfopab  4101  nfopab2  4103  cbvopab1  4106  cbvopab1s  4108  repizf2  4195  copsex2t  4278  copsex2g  4279  euotd  4287  onintrab2im  4554  mosubopt  4728  nfco  4831  dfdmf  4859  dfrnf  4907  nfdm  4910  fv3  5581  nfoprab2  5972  nfoprab3  5973  nfoprab  5974  cbvoprab1  5994  cbvoprab2  5995  cbvoprab3  5998  cnvoprab  6292  ac6sfi  6959  cc3  7335  nfsum1  11521  nfsum  11522  fsum2dlemstep  11599  nfcprod1  11719  nfcprod  11720  fprod2dlemstep  11787  lss1d  13939