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 2835, ax-8 2146. (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 1843	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
3		eq0 4296	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4		df-ral 3077	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	2, 3, 4	3imtr4i 295	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1567   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-dif 4047  df-nul 4279

This theorem is used by:  rexn0  4451  ral0  4453  r19.2zb  4455  raaan  4473  raaanv  4474  raaan2  4477  iinrab2  5027  riinrab  5043  reusv2lem2  5360  cnvpo  6290  dffi3  9426  brdom3  10610  dedekind  11476  fimaxre2  12265  fiminre2  12268  nulchn  18798  mgm0  18839  sgrp0  18921  efgs1  19954  matunitlindf  23001  opnnei  23443  bddiblnc  26167  axcontlem12  29558  nbgr0edg  29943  prcliscplgr  30000  cplgr0v  30013  0vtxrgr  30162  0vconngr  30799  frgr1v  30877  ubthlem1  31477  rdgssun  38394  mbfresfi  38677  blbnd  38814  rrnequiv  38862  upbdrech2  46417  limsupubuz  46816  stoweidlem9  47112  fourierdlem31  47241  chnerlem1  47985  nelsubclem  50274  0funcg2  50292