Theorem rzal 4509

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2811, ax-8 2109. (Revised by Gino Giotto, 2-Sep-2024.)

Assertion

Ref	Expression
rzal	⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rzal

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2726	. . . 4 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
2	1	biimpi 215	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
3		df-clab 2711	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
4		sbv 2092	. . . . . 6 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
5	3, 4	bitri 275	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
6	5	bibi2i 338	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
7		nbfal 1557	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
8		pm2.21 123	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑))
9	7, 8	sylbir 234	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) → (𝑥 ∈ 𝐴 → 𝜑))
10	6, 9	sylbi 216	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥 ∈ 𝐴 → 𝜑))
11	2, 10	sylg 1826	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
12		dfnul4 4325	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
13	12	eqeq2i 2746	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
14		df-ral 3063	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
15	11, 13, 14	3imtr4i 292	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1540   = wceq 1542  ⊥wfal 1554  [wsb 2068   ∈ wcel 2107  {cab 2710  ∀wral 3062  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-dif 3952  df-nul 4324

This theorem is referenced by:  rexn0  4511  ral0  4513  ralf0  4514  ralidmOLD  4516  raaan  4521  raaanv  4522  raaan2  4525  iinrab2  5074  riinrab  5088  reusv2lem2  5398  cnvpo  6287  dffi3  9426  brdom3  10523  dedekind  11377  fimaxre2  12159  fiminre2  12162  mgm0  18575  sgrp0  18618  efgs1  19603  opnnei  22624  bddiblnc  25359  axcontlem12  28233  nbgr0edg  28614  prcliscplgr  28671  cplgr0v  28684  0vtxrgr  28833  0vconngr  29446  frgr1v  29524  ubthlem1  30123  rdgssun  36259  matunitlindf  36486  mbfresfi  36534  blbnd  36655  rrnequiv  36703  upbdrech2  44018  limsupubuz  44429  stoweidlem9  44725  fourierdlem31  44854  upwordnul  45594  upwordsing  45598