Theorem rexn0 4455

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-ne 2958  df-ral 3079  df-rex 3089  df-dif 3905  df-nul 4283

This theorem is used by:  r19.2zb  4459  2reu4  4483  reusv2lem3  5369  eusvobj2  7409  isdrs2  18400  ismnd  18845  slwn0  19748  lbsexg  21357  iunconn  23659  ltsn0  28179  grpon0  30991  filbcmb  38498  isbnd2  38541  rencldnfi  43670  iunconnlem2  45765  stoweidlem14  46850  hoidmvval0  47423  thinciso  50404  ralsn0d  50734  alsralrex  50749  alsraln0  50750