Theorem rzal 4435

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 4291	. 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 4274

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 3893  df-nul 4275

This theorem is referenced by:  rexn0  4437  ral0  4439  r19.2zb  4441  raaan  4459  raaanv  4460  raaan2  4463  iinrab2  5013  riinrab  5027  reusv2lem2  5336  cnvpo  6245  dffi3  9337  brdom3  10441  dedekind  11300  fimaxre2  12092  fiminre2  12095  nulchn  18576  mgm0  18615  sgrp0  18686  efgs1  19701  opnnei  23095  bddiblnc  25819  axcontlem12  29058  nbgr0edg  29440  prcliscplgr  29497  cplgr0v  29510  0vtxrgr  29660  0vconngr  30278  frgr1v  30356  ubthlem1  30956  rdgssun  37708  matunitlindf  37953  mbfresfi  38001  blbnd  38122  rrnequiv  38170  upbdrech2  45759  limsupubuz  46159  stoweidlem9  46455  fourierdlem31  46584  chnerlem1  47328  nelsubclem  49554  0funcg2  49571