Theorem rzal 4295

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
rzal	⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rzal

Step	Hyp	Ref	Expression
1		ne0i 4150	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
2	1	necon2bi 3029	. . 3 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
3	2	pm2.21d 119	. 2 ⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 → 𝜑))
4	3	ralrimiv 3174	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166  ∀wral 3117  ∅c0 4144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-v 3416  df-dif 3801  df-nul 4145

This theorem is referenced by:  ralidm  4297  raaan  4302  iinrab2  4803  riinrab  4816  reusv2lem2  5099  cnvpo  5914  dffi3  8606  brdom3  9665  dedekind  10519  fimaxre2  11299  mgm0  17608  sgrp0  17644  efgs1  18499  opnnei  21295  axcontlem12  26274  nbgr0edg  26654  cplgr0v  26725  0vtxrgr  26874  0vconngr  27569  frgr1v  27652  ubthlem1  28281  matunitlindf  33951  mbfresfi  33999  bddiblnc  34023  blbnd  34128  rrnequiv  34176  upbdrech2  40320  fiminre2  40391  limsupubuz  40740  stoweidlem9  41020  fourierdlem31  41149  raaan2  41961