Theorem rzal 4460

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2146  ∀wral 3082  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-ral 3083  df-dif 3911  df-nul 4290

This theorem is used by:  rexn0  4462  ral0  4464  r19.2zb  4466  raaan  4484  raaanv  4485  raaan2  4488  iinrab2  5039  riinrab  5055  reusv2lem2  5375  cnvpo  6295  dffi3  9401  brdom3  10530  dedekind  11391  fimaxre2  12178  fiminre2  12181  nulchn  18700  mgm0  18739  sgrp0  18814  efgs1  19836  opnnei  23314  bddiblnc  26038  axcontlem12  29362  nbgr0edg  29744  prcliscplgr  29801  cplgr0v  29814  0vtxrgr  29963  0vconngr  30581  frgr1v  30659  ubthlem1  31259  rdgssun  38065  matunitlindf  38310  mbfresfi  38358  blbnd  38479  rrnequiv  38527  upbdrech2  46068  limsupubuz  46468  stoweidlem9  46764  fourierdlem31  46893  chnerlem1  47639  nelsubclem  49886  0funcg2  49903