Theorem rzal 4434

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

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

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 2708

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 2715  df-cleq 2728  df-ral 3052  df-dif 3892  df-nul 4274

This theorem is referenced by:  rexn0  4436  ral0  4438  r19.2zb  4440  raaan  4458  raaanv  4459  raaan2  4462  iinrab2  5012  riinrab  5026  reusv2lem2  5341  cnvpo  6251  dffi3  9344  brdom3  10450  dedekind  11309  fimaxre2  12101  fiminre2  12104  nulchn  18585  mgm0  18624  sgrp0  18695  efgs1  19710  opnnei  23085  bddiblnc  25809  axcontlem12  29044  nbgr0edg  29426  prcliscplgr  29483  cplgr0v  29496  0vtxrgr  29645  0vconngr  30263  frgr1v  30341  ubthlem1  30941  rdgssun  37694  matunitlindf  37939  mbfresfi  37987  blbnd  38108  rrnequiv  38156  upbdrech2  45741  limsupubuz  46141  stoweidlem9  46437  fourierdlem31  46566  chnerlem1  47312  nelsubclem  49542  0funcg2  49559