Theorem nfex 1660

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

Syntax hints:   F/wnf 1483   E.wex 1515

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533

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

This theorem is referenced by:  eeor  1718  cbvexv1  1775  cbvex2  1946  eean  1959  nfsbv  1975  nfeu1  2065  nfeuv  2072  nfel  2357  ceqsex2  2813  nfopab  4113  nfopab2  4115  cbvopab1  4118  cbvopab1s  4120  repizf2  4207  copsex2t  4290  copsex2g  4291  euotd  4300  onintrab2im  4567  mosubopt  4741  nfco  4844  dfdmf  4872  dfrnf  4920  nfdm  4923  fv3  5601  nfoprab2  5997  nfoprab3  5998  nfoprab  5999  cbvoprab1  6019  cbvoprab2  6020  cbvoprab3  6023  cnvoprab  6322  ac6sfi  6997  cc3  7382  nfsum1  11700  nfsum  11701  fsum2dlemstep  11778  nfcprod1  11898  nfcprod  11899  fprod2dlemstep  11966  lss1d  14178