Theorem nfex 1686

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

Syntax hints:   F/wnf 1509   E.wex 1541

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559

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

This theorem is referenced by:  eeor  1743  cbvexv1  1801  cbvex2  1974  eean  1987  nfsbv  2003  nfeu1  2093  nfeuv  2100  nfel  2395  ceqsex2  2857  nfopab  4184  nfopab2  4186  cbvopab1  4189  cbvopab1s  4191  repizf2  4281  copsex2t  4367  copsex2g  4368  euotd  4377  onintrab2im  4646  mosubopt  4821  nfco  4926  dfdmf  4955  dfrnf  5004  nfdm  5007  fv3  5699  nfoprab2  6112  nfoprab3  6113  nfoprab  6114  cbvoprab1  6134  cbvoprab2  6135  cbvoprab3  6138  cnvoprab  6444  ac6sfi  7169  cc3  7599  nfsum1  12071  nfsum  12072  fsum2dlemstep  12150  nfcprod1  12270  nfcprod  12271  fprod2dlemstep  12338  lss1d  14662