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

Theorem rzal 3555
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 3461 . . . 4  |-  ( x  e.  A  ->  A  =/=  (/) )
21necon2bi 2492 . . 3  |-  ( A  =  (/)  ->  -.  x  e.  A )
32pm2.21d 98 . 2  |-  ( A  =  (/)  ->  ( x  e.  A  ->  ph )
)
43ralrimiv 2625 1  |-  ( A  =  (/)  ->  A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   A.wral 2543   (/)c0 3455
This theorem is referenced by:  ralidm  3557  rgenz  3559  ralf0  3560  raaan  3561  raaanv  3562  iinrab2  3965  riinrab  3977  reusv2lem2  4536  cnvpo  5213  dffi3  7184  brdom3  8153  fimaxre2  9702  efgs1  15044  opnnei  16857  ubthlem1  21449  dedekind  24082  nofulllem2  24357  axcontlem12  24603  blbnd  26511  rrnequiv  26559  stoweidlem9  27758  raaan2  27953
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator