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  4102  nfopab2  4104  cbvopab1  4107  cbvopab1s  4109  repizf2  4196  copsex2t  4279  copsex2g  4280  euotd  4288  onintrab2im  4555  mosubopt  4729  nfco  4832  dfdmf  4860  dfrnf  4908  nfdm  4911  fv3  5584  nfoprab2  5976  nfoprab3  5977  nfoprab  5978  cbvoprab1  5998  cbvoprab2  5999  cbvoprab3  6002  cnvoprab  6301  ac6sfi  6968  cc3  7351  nfsum1  11538  nfsum  11539  fsum2dlemstep  11616  nfcprod1  11736  nfcprod  11737  fprod2dlemstep  11804  lss1d  14015