Theorem rexn0 4431

Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2815, ax-8 2121. (Revised by GG, 2-Sep-2024.)

Assertion

Ref	Expression
rexn0	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexn0

Step	Hyp	Ref	Expression
1		dfrex2 3067	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		rzal 4429	. . . 4 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3	2	con3i 154	. . 3 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
4	1, 3	sylbi 218	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅)
5	4	neqned 2942	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935  ∀wral 3054  ∃wrex 3064  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ne 2936  df-ral 3055  df-rex 3065  df-dif 3893  df-nul 4269

This theorem is referenced by:  r19.2zb  4435  2reu4  4459  reusv2lem3  5336  eusvobj2  7355  isdrs2  18270  ismnd  18703  slwn0  19588  lbsexg  21164  iunconn  23418  ltsn0  27923  grpon0  30598  filbcmb  38114  isbnd2  38157  rencldnfi  43273  iunconnlem2  45385  stoweidlem14  46464  hoidmvval0  47037  thinciso  49967