Theorem nfex 1617

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

Syntax hints:   F/wnf 1440   E.wex 1472

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490

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

This theorem is referenced by:  eeor  1675  cbvexv1  1732  cbvex2  1902  eean  1911  nfsbv  1927  nfeu1  2017  nfeuv  2024  nfel  2308  ceqsex2  2752  nfopab  4034  nfopab2  4036  cbvopab1  4039  cbvopab1s  4041  repizf2  4125  copsex2t  4207  copsex2g  4208  euotd  4216  onintrab2im  4479  mosubopt  4653  nfco  4753  dfdmf  4781  dfrnf  4829  nfdm  4832  fv3  5493  nfoprab2  5873  nfoprab3  5874  nfoprab  5875  cbvoprab1  5895  cbvoprab2  5896  cbvoprab3  5899  cnvoprab  6183  ac6sfi  6845  cc3  7190  nfsum1  11264  nfsum  11265  fsum2dlemstep  11342  nfcprod1  11462  nfcprod  11463  fprod2dlemstep  11530