Theorem rzal 4450

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2836, ax-8 2147. (Revised by GG, 2-Sep-2024.)

Assertion

Ref	Expression
rzal	⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rzal

Step	Hyp	Ref	Expression
1		pm2.21 124	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑))
2	1	alimi 1844	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
3		eq0 4297	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4		df-ral 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	2, 3, 4	3imtr4i 295	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∅c0 4279

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 2733

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 2740  df-cleq 2753  df-ral 3078  df-dif 3902  df-nul 4280

This theorem is used by:  rexn0  4452  ral0  4454  r19.2zb  4456  raaan  4474  raaanv  4475  raaan2  4478  iinrab2  5028  riinrab  5044  reusv2lem2  5361  cnvpo  6283  dffi3  9407  brdom3  10588  dedekind  11454  fimaxre2  12243  fiminre2  12246  nulchn  18773  mgm0  18814  sgrp0  18896  efgs1  19929  matunitlindf  22976  opnnei  23418  bddiblnc  26142  axcontlem12  29535  nbgr0edg  29920  prcliscplgr  29977  cplgr0v  29990  0vtxrgr  30139  0vconngr  30776  frgr1v  30854  ubthlem1  31454  rdgssun  38269  mbfresfi  38552  blbnd  38689  rrnequiv  38737  upbdrech2  46267  limsupubuz  46667  stoweidlem9  46963  fourierdlem31  47092  chnerlem1  47836  nelsubclem  50119  0funcg2  50136