Theorem rzal 4447

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 2115. (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 1812	. 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
3		eq0 4302	. 2 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴)
4		df-ral 3052	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	2, 3, 4	3imtr4i 292	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1539   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-dif 3904  df-nul 4286

This theorem is referenced by:  rexn0  4449  ral0  4451  r19.2zb  4453  raaan  4471  raaanv  4472  raaan2  4475  iinrab2  5025  riinrab  5039  reusv2lem2  5344  cnvpo  6245  dffi3  9334  brdom3  10438  dedekind  11296  fimaxre2  12087  fiminre2  12090  nulchn  18542  mgm0  18581  sgrp0  18652  efgs1  19664  opnnei  23064  bddiblnc  25799  axcontlem12  29048  nbgr0edg  29430  prcliscplgr  29487  cplgr0v  29500  0vtxrgr  29650  0vconngr  30268  frgr1v  30346  ubthlem1  30945  rdgssun  37579  matunitlindf  37815  mbfresfi  37863  blbnd  37984  rrnequiv  38032  upbdrech2  45552  limsupubuz  45953  stoweidlem9  46249  fourierdlem31  46378  chnerlem1  47122  nelsubclem  49308  0funcg2  49325