Theorem rzal 4453

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

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

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 2155  ax-ext 2734

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 2741  df-cleq 2754  df-ral 3079  df-dif 3905  df-nul 4283

This theorem is used by:  rexn0  4455  ral0  4457  r19.2zb  4459  raaan  4477  raaanv  4478  raaan2  4481  iinrab2  5032  riinrab  5048  reusv2lem2  5368  cnvpo  6289  dffi3  9405  brdom3  10535  dedekind  11401  fimaxre2  12188  fiminre2  12191  nulchn  18713  mgm0  18754  sgrp0  18835  efgs1  19868  matunitlindf  22909  opnnei  23351  bddiblnc  26076  axcontlem12  29440  nbgr0edg  29825  prcliscplgr  29882  cplgr0v  29895  0vtxrgr  30044  0vconngr  30681  frgr1v  30759  ubthlem1  31359  rdgssun  38140  mbfresfi  38423  blbnd  38545  rrnequiv  38593  upbdrech2  46149  limsupubuz  46549  stoweidlem9  46845  fourierdlem31  46974  chnerlem1  47718  nelsubclem  50001  0funcg2  50018