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

Syntax hints:   F/wnf 1513   E.wex 1545

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563

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

This theorem is referenced by:  eeor  1747  cbvexv1  1805  cbvex2  1978  eean  1991  nfsbv  2007  nfeu1  2097  nfeuv  2104  nfel  2401  ceqsex2  2863  nfopab  4194  nfopab2  4196  cbvopab1  4199  cbvopab1s  4201  repizf2  4294  copsex2t  4380  copsex2g  4381  euotd  4390  onintrab2im  4660  mosubopt  4835  nfco  4940  dfdmf  4969  dfrnf  5018  nfdm  5021  fv3  5713  nfoprab2  6128  nfoprab3  6129  nfoprab  6130  cbvoprab1  6150  cbvoprab2  6151  cbvoprab3  6154  cnvoprab  6460  ac6sfi  7192  cc3  7624  nfsum1  12100  nfsum  12101  fsum2dlemstep  12179  nfcprod1  12299  nfcprod  12300  fprod2dlemstep  12367  lss1d  14692