Theorem nfex 1843

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

Hypothesis

Ref	Expression
nfal.1	⊢ Ⅎxφ

Assertion

Ref	Expression
nfex	⊢ Ⅎx∃yφ

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		nfal.1	. . . 4 ⊢ Ⅎxφ
2	1	nfri 1762	. . 3 ⊢ (φ → ∀xφ)
3	2	hbex 1841	. 2 ⊢ (∃yφ → ∀x∃yφ)
4	3	nfi 1551	1 ⊢ Ⅎx∃yφ

Syntax hints:  ∃wex 1541  Ⅎ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  2498  ceqsex2  2896  copsex2t  4609  copsex2g  4610  mosubopt  4613  nfopab  4628  nfopab2  4630  cbvopab1  4633  cbvopab1s  4635  nfco  4883  dfdmf  4906  dfrnf  4963  fv3  5342  nfoprab2  5548  nfoprab3  5549  nfoprab  5550  cbvoprab1  5568  cbvoprab2  5569  cbvoprab3  5572