Theorem nfex 1843

Description: If x is not free in ph, it is not free in E.yph. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

Hypothesis

Ref	Expression
nfal.1	|- F/xph

Assertion

Ref	Expression
nfex	|- F/xE.yph

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 |- F/xph
2	1	nfri 1762	. . 3 |- (ph -> A.xph)
3	2	hbex 1841	. 2 |- (E.yph -> A.xE.yph)
4	3	nfi 1551	1 |- F/xE.yph

Syntax hints:  E.wex 1541   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  19.12  1847  excomimOLD  1858  eeor  1885  eean  1912  cbvex2  2005  nfeu1  2214  moexex  2273  nfel  2497  ceqsex2  2895  copsex2t  4608  copsex2g  4609  mosubopt  4612  nfopab  4627  nfopab2  4629  cbvopab1  4632  cbvopab1s  4634  nfco  4882  dfdmf  4905  dfrnf  4962  fv3  5341  nfoprab2  5547  nfoprab3  5548  nfoprab  5549  cbvoprab1  5567  cbvoprab2  5568  cbvoprab3  5571