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 2839, ax-8 2149. (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 3081	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
5	2, 3, 4	3imtr4i 295	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-dif 4050  df-nul 4282

This theorem is used by:  rexn0  4455  ral0  4457  r19.2zb  4459  raaan  4477  raaanv  4478  raaan2  4481  iinrab2  5031  riinrab  5047  reusv2lem2  5365  cnvpo  6308  dffi3  9450  brdom3  10634  dedekind  11500  fimaxre2  12289  fiminre2  12292  nulchn  18822  mgm0  18863  sgrp0  18945  efgs1  19979  matunitlindf  23026  opnnei  23468  bddiblnc  26192  axcontlem12  29583  nbgr0edg  29968  prcliscplgr  30025  cplgr0v  30038  0vtxrgr  30187  0vconngr  30824  frgr1v  30902  ubthlem1  31502  rdgssun  38493  mbfresfi  38776  blbnd  38913  rrnequiv  38961  upbdrech2  46529  limsupubuz  46928  stoweidlem9  47224  fourierdlem31  47353  chnerlem1  48097  nelsubclem  50386  0funcg2  50404