Theorem rexn0 4449

Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2836, ax-8 2143. (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 3088	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		rzal 4447	. . . 4 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3	2	con3i 154	. . 3 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
4	1, 3	sylbi 219	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅)
5	4	neqned 2963	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956  ∀wral 3075  ∃wrex 3085  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-ne 2957  df-ral 3076  df-rex 3086  df-dif 3907  df-nul 4286

This theorem is referenced by:  r19.2zb  4453  2reu4  4477  reusv2lem3  5356  eusvobj2  7384  isdrs2  18321  ismnd  18754  slwn0  19638  lbsexg  21214  iunconn  23468  ltsn0  27976  grpon0  30651  filbcmb  38203  isbnd2  38246  rencldnfi  43362  iunconnlem2  45474  stoweidlem14  46552  hoidmvval0  47125  thinciso  50055