Theorem nfex 1683

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

Syntax hints:   F/wnf 1506   E.wex 1538

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556

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

This theorem is referenced by:  eeor  1741  cbvexv1  1798  cbvex2  1969  eean  1982  nfsbv  1998  nfeu1  2088  nfeuv  2095  nfel  2381  ceqsex2  2841  nfopab  4152  nfopab2  4154  cbvopab1  4157  cbvopab1s  4159  repizf2  4246  copsex2t  4331  copsex2g  4332  euotd  4341  onintrab2im  4610  mosubopt  4784  nfco  4887  dfdmf  4916  dfrnf  4965  nfdm  4968  fv3  5650  nfoprab2  6054  nfoprab3  6055  nfoprab  6056  cbvoprab1  6076  cbvoprab2  6077  cbvoprab3  6080  cnvoprab  6380  ac6sfi  7060  cc3  7454  nfsum1  11867  nfsum  11868  fsum2dlemstep  11945  nfcprod1  12065  nfcprod  12066  fprod2dlemstep  12133  lss1d  14347