Theorem nfex 2262

Description: If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex 2262, hbex 2263. (Revised by Wolf Lammen, 16-Oct-2021.)

Hypothesis

Ref	Expression
nfex.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfex	⊢ Ⅎ𝑥∃𝑦𝜑

Proof of Theorem nfex

Step	Hyp	Ref	Expression
1		df-ex 1743	. 2 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
2		nfex.1	. . . . 5 ⊢ Ⅎ𝑥𝜑
3	2	nfn 1819	. . . 4 ⊢ Ⅎ𝑥 ¬ 𝜑
4	3	nfal 2261	. . 3 ⊢ Ⅎ𝑥∀𝑦 ¬ 𝜑
5	4	nfn 1819	. 2 ⊢ Ⅎ𝑥 ¬ ∀𝑦 ¬ 𝜑
6	1, 5	nfxfr 1815	1 ⊢ Ⅎ𝑥∃𝑦𝜑

Syntax hints:  ¬ wn 3  ∀wal 1505  ∃wex 1742  Ⅎwnf 1746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-10 2077  ax-11 2091  ax-12 2104

This theorem depends on definitions:  df-bi 199  df-or 834  df-ex 1743  df-nf 1747

This theorem is referenced by:  hbex  2263  nfnf  2264  19.12  2265  eeor  2272  eean  2280  eeeanv  2282  nfmo1  2566  nfeu1  2602  2moswapv  2657  moexex  2664  r19.12  3259  ceqsex2  3458  nfopab  4991  nfopab2  4993  cbvopab1  4996  cbvopab1s  4998  axrep2  5046  axrep3  5047  axrep4  5048  copsex2t  5232  copsex2g  5233  mosubopt  5249  euotd  5252  nfco  5579  dfdmf  5608  dfrnf  5656  nfdm  5659  fv3  6511  oprabv  7027  nfoprab2  7029  nfoprab3  7030  nfoprab  7031  cbvoprab1  7051  cbvoprab2  7052  cbvoprab3  7055  nfwrecs  7745  ac6sfi  8549  aceq1  9329  zfcndrep  9826  zfcndinf  9830  nfsum1  14897  nfsum  14898  fsum2dlem  14975  nfcprod1  15114  nfcprod  15115  fprod2dlem  15184  brabgaf  30113  cnvoprabOLD  30197  bnj981  31830  bnj1388  31911  bnj1445  31922  bnj1489  31934  nffrecs  32581  bj-axrep2  33559  bj-axrep3  33560  bj-axrep4  33561  pm11.71  40090  upbdrech  40947  stoweidlem57  41719  or2expropbi  42620  ich2exprop  42941  ichnreuop  42942  ichreuopeq  42943  reuopreuprim  42996