Theorem rzal 4502

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541  ⊥wfal 1553  [wsb 2067   ∈ wcel 2106  {cab 2708  ∀wral 3060  ∅c0 4318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-ral 3061  df-dif 3947  df-nul 4319

This theorem is referenced by:  rexn0  4504  ral0  4506  ralf0  4507  ralidmOLD  4509  raaan  4514  raaanv  4515  raaan2  4518  iinrab2  5066  riinrab  5080  reusv2lem2  5390  cnvpo  6275  dffi3  9408  brdom3  10505  dedekind  11359  fimaxre2  12141  fiminre2  12144  mgm0  18557  sgrp0  18599  efgs1  19567  opnnei  22553  bddiblnc  25288  axcontlem12  28098  nbgr0edg  28479  prcliscplgr  28536  cplgr0v  28549  0vtxrgr  28698  0vconngr  29311  frgr1v  29389  ubthlem1  29986  rdgssun  36061  matunitlindf  36288  mbfresfi  36336  blbnd  36458  rrnequiv  36506  upbdrech2  43789  limsupubuz  44200  stoweidlem9  44496  fourierdlem31  44625  upwordnul  45365  upwordsing  45369