Theorem rzal 4459

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2806, ax-8 2113. (Revised by GG, 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 2724	. . . 4 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
2	1	biimpi 216	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}))
3		df-clab 2710	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
4		sbv 2091	. . . . . 6 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
5	3, 4	bitri 275	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
6	5	bibi2i 337	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
7		nbfal 1556	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
8		pm2.21 123	. . . . 5 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑))
9	7, 8	sylbir 235	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) → (𝑥 ∈ 𝐴 → 𝜑))
10	6, 9	sylbi 217	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥 ∈ 𝐴 → 𝜑))
11	2, 10	sylg 1824	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
12		dfnul4 4285	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
13	12	eqeq2i 2744	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
14		df-ral 3048	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
15	11, 13, 14	3imtr4i 292	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  ⊥wfal 1553  [wsb 2067   ∈ wcel 2111  {cab 2709  ∀wral 3047  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ral 3048  df-dif 3905  df-nul 4284

This theorem is referenced by:  rexn0  4461  ral0  4463  ralf0  4464  raaan  4467  raaanv  4468  raaan2  4471  iinrab2  5018  riinrab  5032  reusv2lem2  5337  cnvpo  6234  dffi3  9315  brdom3  10416  dedekind  11273  fimaxre2  12064  fiminre2  12067  nulchn  18522  mgm0  18561  sgrp0  18632  efgs1  19645  opnnei  23033  bddiblnc  25768  axcontlem12  28951  nbgr0edg  29333  prcliscplgr  29390  cplgr0v  29403  0vtxrgr  29553  0vconngr  30168  frgr1v  30246  ubthlem1  30845  rdgssun  37411  matunitlindf  37657  mbfresfi  37705  blbnd  37826  rrnequiv  37874  upbdrech2  45348  limsupubuz  45750  stoweidlem9  46046  fourierdlem31  46175  nelsubclem  49098  0funcg2  49115