Theorem rexn0 4486

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-ne 2933  df-ral 3052  df-rex 3061  df-dif 3929  df-nul 4309

This theorem is referenced by:  2reu4  4498  reusv2lem3  5370  eusvobj2  7397  isdrs2  18318  ismnd  18715  slwn0  19596  lbsexg  21125  iunconn  23366  sltn0  27869  grpon0  30483  filbcmb  37764  isbnd2  37807  rencldnfi  42844  iunconnlem2  44959  stoweidlem14  46043  hoidmvval0  46616  thinciso  49356