Theorem nfex 1861

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
nfal.1	|- F/ x ph

Assertion

Ref	Expression
nfex	|- F/ x E. y ph

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 |- F/ x ph
2	1	nfri 1774	. . 3 |- ( ph -> A. x ph )
3	2	hbex 1859	. 2 |- ( E. y ph -> A. x E. y ph )
4	3	nfi 1557	1 |- F/ x E. y ph

Syntax hints:   E.wex 1547   F/wnf 1550

This theorem is referenced by:  19.12  1865  excomimOLD  1877  eeor  1903  eean  1932  eeeanv  1934  cbvex2  2055  nfeu1  2264  moexex  2323  nfel  2548  ceqsex2  2952  nfopab  4233  nfopab2  4235  cbvopab1  4238  cbvopab1s  4240  axrep2  4282  axrep3  4283  axrep4  4284  copsex2t  4403  copsex2g  4404  mosubopt  4414  euotd  4417  nfco  4997  dfdmf  5023  dfrnf  5067  nfdm  5070  fv3  5703  nfoprab2  6083  nfoprab3  6084  nfoprab  6085  cbvoprab1  6103  cbvoprab2  6104  cbvoprab3  6107  ac6sfi  7310  aceq1  7954  zfcndrep  8445  zfcndinf  8449  nfsum1  12439  nfsum  12440  fsum2dlem  12509  nfcprod1  25189  nfcprod  25190  fprod2dlem  25257  pm11.71  27464  stoweidlem57  27673  bnj981  29027  bnj1388  29108  bnj1445  29119  bnj1489  29131

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551