Theorem rzal 4436

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2817, ax-8 2110. (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 2731	. . . 4 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
2	1	biimpi 215	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
3		df-clab 2716	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
4		sbv 2092	. . . . . 6 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
5	3, 4	bitri 274	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
6	5	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
7		nbfal 1554	. . . . 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 4255	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
13	12	eqeq2i 2751	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
14		df-ral 3068	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
15	11, 13, 14	3imtr4i 291	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ⊥wfal 1551  [wsb 2068   ∈ wcel 2108  {cab 2715  ∀wral 3063  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3068  df-dif 3886  df-nul 4254

This theorem is referenced by:  rexn0  4438  ral0  4440  ralf0  4441  ralidmOLD  4443  raaan  4448  raaanv  4449  raaan2  4452  iinrab2  4995  riinrab  5009  reusv2lem2  5317  cnvpo  6179  dffi3  9120  brdom3  10215  dedekind  11068  fimaxre2  11850  fiminre2  11853  mgm0  18255  sgrp0  18297  efgs1  19256  opnnei  22179  bddiblnc  24911  axcontlem12  27246  nbgr0edg  27627  prcliscplgr  27684  cplgr0v  27697  0vtxrgr  27846  0vconngr  28458  frgr1v  28536  ubthlem1  29133  rdgssun  35476  matunitlindf  35702  mbfresfi  35750  blbnd  35872  rrnequiv  35920  upbdrech2  42737  limsupubuz  43144  stoweidlem9  43440  fourierdlem31  43569