Theorem nfex 1630

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

Syntax hints:   F/wnf 1453   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  eeor  1688  cbvexv1  1745  cbvex2  1915  eean  1924  nfsbv  1940  nfeu1  2030  nfeuv  2037  nfel  2321  ceqsex2  2770  nfopab  4057  nfopab2  4059  cbvopab1  4062  cbvopab1s  4064  repizf2  4148  copsex2t  4230  copsex2g  4231  euotd  4239  onintrab2im  4502  mosubopt  4676  nfco  4776  dfdmf  4804  dfrnf  4852  nfdm  4855  fv3  5519  nfoprab2  5903  nfoprab3  5904  nfoprab  5905  cbvoprab1  5925  cbvoprab2  5926  cbvoprab3  5929  cnvoprab  6213  ac6sfi  6876  cc3  7230  nfsum1  11319  nfsum  11320  fsum2dlemstep  11397  nfcprod1  11517  nfcprod  11518  fprod2dlemstep  11585