Theorem rzal 4429

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1545   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-ral 3055  df-dif 3893  df-nul 4269

This theorem is referenced by:  rexn0  4431  ral0  4433  r19.2zb  4435  raaan  4453  raaanv  4454  raaan2  4457  iinrab2  5006  riinrab  5020  reusv2lem2  5335  cnvpo  6245  dffi3  9341  brdom3  10448  dedekind  11307  fimaxre2  12099  fiminre2  12102  nulchn  18583  mgm0  18622  sgrp0  18693  efgs1  19708  opnnei  23110  bddiblnc  25834  axcontlem12  29069  nbgr0edg  29451  prcliscplgr  29508  cplgr0v  29521  0vtxrgr  29670  0vconngr  30288  frgr1v  30366  ubthlem1  30966  rdgssun  37747  matunitlindf  37992  mbfresfi  38040  blbnd  38161  rrnequiv  38209  upbdrech2  45763  limsupubuz  46163  stoweidlem9  46459  fourierdlem31  46588  chnerlem1  47334  nelsubclem  49564  0funcg2  49581