Theorem nfex 1637

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

Syntax hints:   F/wnf 1460   E.wex 1492

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510

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

This theorem is referenced by:  eeor  1695  cbvexv1  1752  cbvex2  1922  eean  1931  nfsbv  1947  nfeu1  2037  nfeuv  2044  nfel  2328  ceqsex2  2777  nfopab  4069  nfopab2  4071  cbvopab1  4074  cbvopab1s  4076  repizf2  4160  copsex2t  4243  copsex2g  4244  euotd  4252  onintrab2im  4515  mosubopt  4689  nfco  4789  dfdmf  4817  dfrnf  4865  nfdm  4868  fv3  5535  nfoprab2  5920  nfoprab3  5921  nfoprab  5922  cbvoprab1  5942  cbvoprab2  5943  cbvoprab3  5946  cnvoprab  6230  ac6sfi  6893  cc3  7262  nfsum1  11355  nfsum  11356  fsum2dlemstep  11433  nfcprod1  11553  nfcprod  11554  fprod2dlemstep  11621