Theorem rzal 4458

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2808, ax-8 2115. (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		biidd 262	. . . . 5 ⊢ (𝑦 = 𝑥 → (⊥ ↔ ⊥))
2	1	eqabbw 2806	. . . 4 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
3	2	biimpi 216	. . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥))
4		nbfal 1556	. . . 4 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥))
5		pm2.21 123	. . . 4 ⊢ (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → 𝜑))
6	4, 5	sylbir 235	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) → (𝑥 ∈ 𝐴 → 𝜑))
7	3, 6	sylg 1824	. 2 ⊢ (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
8		dfnul4 4284	. . 3 ⊢ ∅ = {𝑦 ∣ ⊥}
9	8	eqeq2i 2746	. 2 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
10		df-ral 3049	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
11	7, 9, 10	3imtr4i 292	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541  ⊥wfal 1553   ∈ wcel 2113  {cab 2711  ∀wral 3048  ∅c0 4282

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 2123  ax-ext 2705

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 2712  df-cleq 2725  df-ral 3049  df-dif 3901  df-nul 4283

This theorem is referenced by:  rexn0  4460  ral0  4462  ralf0  4463  raaan  4466  raaanv  4467  raaan2  4470  iinrab2  5020  riinrab  5034  reusv2lem2  5339  cnvpo  6239  dffi3  9322  brdom3  10426  dedekind  11283  fimaxre2  12074  fiminre2  12077  nulchn  18527  mgm0  18566  sgrp0  18637  efgs1  19649  opnnei  23036  bddiblnc  25771  axcontlem12  28955  nbgr0edg  29337  prcliscplgr  29394  cplgr0v  29407  0vtxrgr  29557  0vconngr  30175  frgr1v  30253  ubthlem1  30852  rdgssun  37443  matunitlindf  37678  mbfresfi  37726  blbnd  37847  rrnequiv  37895  upbdrech2  45433  limsupubuz  45835  stoweidlem9  46131  fourierdlem31  46260  chnerlem1  47004  nelsubclem  49192  0funcg2  49209