Theorem rzal 4456

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wal 1568   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ral 3080  df-dif 3909  df-nul 4288

This theorem is referenced by:  rexn0  4458  ral0  4460  r19.2zb  4462  raaan  4480  raaanv  4481  raaan2  4484  iinrab2  5035  riinrab  5051  reusv2lem2  5372  cnvpo  6290  dffi3  9392  brdom3  10513  dedekind  11374  fimaxre2  12161  fiminre2  12164  nulchn  18676  mgm0  18715  sgrp0  18786  efgs1  19806  opnnei  23258  bddiblnc  25982  axcontlem12  29303  nbgr0edg  29685  prcliscplgr  29742  cplgr0v  29755  0vtxrgr  29904  0vconngr  30522  frgr1v  30600  ubthlem1  31200  rdgssun  38002  matunitlindf  38247  mbfresfi  38295  blbnd  38416  rrnequiv  38464  upbdrech2  46007  limsupubuz  46407  stoweidlem9  46703  fourierdlem31  46832  chnerlem1  47578  nelsubclem  49822  0funcg2  49839