Theorem nfex 1690

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

This proof depends on syntax axioms:   F/wnf 1513   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  eeor  1747  cbvexv1  1805  cbvex2  1978  eean  1991  nfsbv  2007  nfeu1  2097  nfeuv  2104  nfel  2401  ceqsex2  2863  nfopab  4200  nfopab2  4202  cbvopab1  4205  cbvopab1s  4207  repizf2  4301  copsex2t  4387  copsex2g  4388  euotd  4397  onintrab2im  4667  mosubopt  4842  nfco  4947  dfdmf  4976  dfrnf  5025  nfdm  5028  fv3  5721  nfoprab2  6141  nfoprab3  6142  nfoprab  6143  cbvoprab1  6163  cbvoprab2  6164  cbvoprab3  6167  cnvoprab  6474  ac6sfi  7206  cc3  7640  nfsum1  12147  nfsum  12148  fsum2dlemstep  12226  nfcprod1  12346  nfcprod  12347  fprod2dlemstep  12414  lss1d  14829  nfals  17351