Theorem rzal 4447

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 2143. (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 123	. . 3 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑))
2	1	alimi 1830	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
3		eq0 4302	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4		df-ral 3076	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	2, 3, 4	3imtr4i 294	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1557   = wceq 1559   ∈ wcel 2141  ∀wral 3075  ∅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-ral 3076  df-dif 3907  df-nul 4286

This theorem is referenced by:  rexn0  4449  ral0  4451  r19.2zb  4453  raaan  4471  raaanv  4472  raaan2  4475  iinrab2  5026  riinrab  5040  reusv2lem2  5355  cnvpo  6270  dffi3  9374  brdom3  10482  dedekind  11343  fimaxre2  12134  fiminre2  12137  nulchn  18634  mgm0  18673  sgrp0  18744  efgs1  19758  opnnei  23160  bddiblnc  25884  axcontlem12  29122  nbgr0edg  29504  prcliscplgr  29561  cplgr0v  29574  0vtxrgr  29723  0vconngr  30341  frgr1v  30419  ubthlem1  31019  rdgssun  37836  matunitlindf  38081  mbfresfi  38129  blbnd  38250  rrnequiv  38298  upbdrech2  45851  limsupubuz  46251  stoweidlem9  46547  fourierdlem31  46676  chnerlem1  47422  nelsubclem  49652  0funcg2  49669