Theorem nfex 1568

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

Syntax hints:   F/wnf 1389   E.wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  eeor  1625  cbvex2  1838  eean  1847  nfeu1  1952  nfeuv  1959  nfel  2227  ceqsex2  2639  nfopab  3846  nfopab2  3848  cbvopab1  3851  cbvopab1s  3853  repizf2  3936  copsex2t  4000  copsex2g  4001  euotd  4009  onintrab2im  4262  mosubopt  4423  nfco  4519  dfdmf  4546  dfrnf  4593  nfdm  4596  fv3  5218  nfoprab2  5575  nfoprab3  5576  nfoprab  5577  cbvoprab1  5596  cbvoprab2  5597  cbvoprab3  5600  cnvoprab  5875  ac6sfi  6379  nfsum1  10193  nfsum  10194