MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rzal Structured version   Visualization version   GIF version

Theorem rzal 4514
Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Avoid df-clel 2813, ax-8 2107. (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.
StepHypRef Expression
1 dfcleq 2727 . . . 4 (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
21biimpi 216 . . 3 (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}))
3 df-clab 2712 . . . . . 6 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
4 sbv 2085 . . . . . 6 ([𝑥 / 𝑦]⊥ ↔ ⊥)
53, 4bitri 275 . . . . 5 (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥)
65bibi2i 337 . . . 4 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥𝐴 ↔ ⊥))
7 nbfal 1551 . . . . 5 𝑥𝐴 ↔ (𝑥𝐴 ↔ ⊥))
8 pm2.21 123 . . . . 5 𝑥𝐴 → (𝑥𝐴𝜑))
97, 8sylbir 235 . . . 4 ((𝑥𝐴 ↔ ⊥) → (𝑥𝐴𝜑))
106, 9sylbi 217 . . 3 ((𝑥𝐴𝑥 ∈ {𝑦 ∣ ⊥}) → (𝑥𝐴𝜑))
112, 10sylg 1819 . 2 (𝐴 = {𝑦 ∣ ⊥} → ∀𝑥(𝑥𝐴𝜑))
12 dfnul4 4340 . . 3 ∅ = {𝑦 ∣ ⊥}
1312eqeq2i 2747 . 2 (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥})
14 df-ral 3059 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
1511, 13, 143imtr4i 292 1 (𝐴 = ∅ → ∀𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wal 1534   = wceq 1536  wfal 1548  [wsb 2061  wcel 2105  {cab 2711  wral 3058  c0 4338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-ral 3059  df-dif 3965  df-nul 4339
This theorem is referenced by:  rexn0  4516  ral0  4518  ralf0  4519  raaan  4522  raaanv  4523  raaan2  4526  iinrab2  5074  riinrab  5088  reusv2lem2  5404  cnvpo  6308  dffi3  9468  brdom3  10565  dedekind  11421  fimaxre2  12210  fiminre2  12213  mgm0  18681  sgrp0  18752  efgs1  19767  opnnei  23143  bddiblnc  25891  axcontlem12  29004  nbgr0edg  29388  prcliscplgr  29445  cplgr0v  29458  0vtxrgr  29608  0vconngr  30221  frgr1v  30299  ubthlem1  30898  rdgssun  37360  matunitlindf  37604  mbfresfi  37652  blbnd  37773  rrnequiv  37821  upbdrech2  45258  limsupubuz  45668  stoweidlem9  45964  fourierdlem31  46093  upwordnul  46833  upwordsing  46837
  Copyright terms: Public domain W3C validator