Theorem rzal 4411

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 4250	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐴 ≠ ∅)
2	1	necon2bi 3017	. . 3 ⊢ (𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴)
3	2	pm2.21d 121	. 2 ⊢ (𝐴 = ∅ → (𝑥 ∈ 𝐴 → 𝜑))
4	3	ralrimiv 3148	1 ⊢ (𝐴 = ∅ → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∅c0 4243

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-dif 3884  df-nul 4244

This theorem is referenced by:  ralidm  4413  raaan  4418  raaanv  4419  raaan2  4422  iinrab2  4955  riinrab  4969  reusv2lem2  5265  cnvpo  6106  dffi3  8879  brdom3  9939  dedekind  10792  fimaxre2  11574  mgm0  17858  sgrp0  17900  efgs1  18853  opnnei  21725  bddiblnc  24445  axcontlem12  26769  nbgr0edg  27147  prcliscplgr  27204  cplgr0v  27217  0vtxrgr  27366  0vconngr  27978  frgr1v  28056  ubthlem1  28653  rdgssun  34795  matunitlindf  35055  mbfresfi  35103  blbnd  35225  rrnequiv  35273  upbdrech2  41940  fiminre2  42010  limsupubuz  42355  stoweidlem9  42651  fourierdlem31  42780