Theorem rexn0 4458

Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) Avoid df-clel 2838, ax-8 2145. (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 3092	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2		rzal 4456	. . . 4 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3	2	con3i 155	. . 3 ⊢ (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ 𝐴 = ∅)
4	1, 3	sylbi 220	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ 𝐴 = ∅)
5	4	neqned 2965	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝐴 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ne 2959  df-ral 3080  df-rex 3090  df-dif 3909  df-nul 4288

This theorem is referenced by:  r19.2zb  4462  2reu4  4486  reusv2lem3  5373  eusvobj2  7404  isdrs2  18363  ismnd  18796  slwn0  19686  lbsexg  21269  iunconn  23566  ltsn0  28080  grpon0  30835  filbcmb  38372  isbnd2  38415  rencldnfi  43531  iunconnlem2  45626  stoweidlem14  46711  hoidmvval0  47284  thinciso  50231  ralsn0d  50558  alsralrex  50573  alsraln0  50574