Theorem rzal 4451

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1561   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ral 3080  df-dif 3910  df-nul 4289

This theorem is referenced by:  rexn0  4453  ral0  4455  r19.2zb  4457  raaan  4475  raaanv  4476  raaan2  4479  iinrab2  5030  riinrab  5046  reusv2lem2  5361  cnvpo  6278  dffi3  9379  brdom3  10500  dedekind  11361  fimaxre2  12151  fiminre2  12154  nulchn  18665  mgm0  18704  sgrp0  18775  efgs1  19796  opnnei  23238  bddiblnc  25962  axcontlem12  29234  nbgr0edg  29616  prcliscplgr  29673  cplgr0v  29686  0vtxrgr  29835  0vconngr  30453  frgr1v  30531  ubthlem1  31131  rdgssun  37884  matunitlindf  38129  mbfresfi  38177  blbnd  38298  rrnequiv  38346  upbdrech2  45885  limsupubuz  46285  stoweidlem9  46581  fourierdlem31  46710  chnerlem1  47456  nelsubclem  49696  0funcg2  49713