Theorem rzal 4472

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ⊥wfal 1552  [wsb 2065   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-dif 3917  df-nul 4297

This theorem is referenced by:  rexn0  4474  ral0  4476  ralf0  4477  raaan  4480  raaanv  4481  raaan2  4484  iinrab2  5034  riinrab  5048  reusv2lem2  5354  cnvpo  6260  dffi3  9382  brdom3  10481  dedekind  11337  fimaxre2  12128  fiminre2  12131  mgm0  18583  sgrp0  18654  efgs1  19665  opnnei  23007  bddiblnc  25743  axcontlem12  28902  nbgr0edg  29284  prcliscplgr  29341  cplgr0v  29354  0vtxrgr  29504  0vconngr  30122  frgr1v  30200  ubthlem1  30799  rdgssun  37366  matunitlindf  37612  mbfresfi  37660  blbnd  37781  rrnequiv  37829  upbdrech2  45306  limsupubuz  45711  stoweidlem9  46007  fourierdlem31  46136  upwordnul  46878  upwordsing  46882  nelsubclem  49056  0funcg2  49073