Theorem rzal 4449

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2812, ax-8 2116. (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 1813	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
3		eq0 4304	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4		df-ral 3053	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	2, 3, 4	3imtr4i 292	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1540   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-dif 3906  df-nul 4288

This theorem is referenced by:  rexn0  4451  ral0  4453  r19.2zb  4455  raaan  4473  raaanv  4474  raaan2  4477  iinrab2  5027  riinrab  5041  reusv2lem2  5346  cnvpo  6253  dffi3  9346  brdom3  10450  dedekind  11308  fimaxre2  12099  fiminre2  12102  nulchn  18554  mgm0  18593  sgrp0  18664  efgs1  19676  opnnei  23076  bddiblnc  25811  axcontlem12  29060  nbgr0edg  29442  prcliscplgr  29499  cplgr0v  29512  0vtxrgr  29662  0vconngr  30280  frgr1v  30358  ubthlem1  30957  rdgssun  37627  matunitlindf  37863  mbfresfi  37911  blbnd  38032  rrnequiv  38080  upbdrech2  45664  limsupubuz  46065  stoweidlem9  46361  fourierdlem31  46490  chnerlem1  47234  nelsubclem  49420  0funcg2  49437