Theorem rzal 4264

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 4119	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
2	1	necon2bi 2999	. . 3 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
3	2	pm2.21d 119	. 2 ⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 → 𝜑))
4	3	ralrimiv 3144	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   = wceq 1653   ∈ wcel 2157  ∀wral 3087  ∅c0 4113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-v 3385  df-dif 3770  df-nul 4114

This theorem is referenced by:  ralidm  4266  raaan  4271  iinrab2  4771  riinrab  4784  reusv2lem2  5067  cnvpo  5890  dffi3  8577  brdom3  9636  dedekind  10488  fimaxre2  11259  mgm0  17567  sgrp0  17603  efgs1  18458  opnnei  21250  axcontlem12  26204  nbgr0edg  26587  cplgr0v  26669  0vtxrgr  26818  0vconngr  27529  frgr1v  27612  ubthlem1  28243  matunitlindf  33888  mbfresfi  33936  bddiblnc  33960  blbnd  34065  rrnequiv  34113  upbdrech2  40255  fiminre2  40326  limsupubuz  40677  stoweidlem9  40957  fourierdlem31  41086  raaan2  41901