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

Theorem rzal 3870
Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
rzal  |-  ( A  =  (/)  ->  A. x  e.  A  ph )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem rzal
StepHypRef Expression
1 ne0i 3736 . . . 4  |-  ( x  e.  A  ->  A  =/=  (/) )
21necon2bi 2653 . . 3  |-  ( A  =  (/)  ->  -.  x  e.  A )
32pm2.21d 110 . 2  |-  ( A  =  (/)  ->  ( x  e.  A  ->  ph )
)
43ralrimiv 2799 1  |-  ( A  =  (/)  ->  A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1443    e. wcel 1886   A.wral 2736   (/)c0 3730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-v 3046  df-dif 3406  df-nul 3731
This theorem is referenced by:  ralidm  3872  rgenz  3874  ralf0  3875  raaan  3876  raaanv  3877  iinrab2  4340  riinrab  4353  reusv2lem2  4604  cnvpo  5373  dffi3  7942  brdom3  8953  dedekind  9794  fimaxre2  10549  efgs1  17378  opnnei  20129  axcontlem12  24998  ubthlem1  26505  nofulllem2  30585  mbfresfi  31980  bddiblnc  32005  blbnd  32112  rrnequiv  32160  upbdrech2  37520  stoweidlem9  37863  fourierdlem31  37994  fourierdlem31OLD  37995  raaan2  38590  nbgr0edg  39408  0vtxrgr  39575
  Copyright terms: Public domain W3C validator