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

Theorem rzal 3935
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 3796 . . . 4  |-  ( x  e.  A  ->  A  =/=  (/) )
21necon2bi 2704 . . 3  |-  ( A  =  (/)  ->  -.  x  e.  A )
32pm2.21d 106 . 2  |-  ( A  =  (/)  ->  ( x  e.  A  ->  ph )
)
43ralrimiv 2879 1  |-  ( A  =  (/)  ->  A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   A.wral 2817   (/)c0 3790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-v 3120  df-dif 3484  df-nul 3791
This theorem is referenced by:  ralidm  3937  rgenz  3939  ralf0  3940  raaan  3941  raaanv  3942  iinrab2  4394  riinrab  4407  reusv2lem2  4655  cnvpo  5551  dffi3  7903  brdom3  8918  dedekind  9755  fimaxre2  10503  efgs1  16626  opnnei  19489  axcontlem12  24101  ubthlem1  25609  nofulllem2  29390  mbfresfi  29988  bddiblnc  30012  blbnd  30210  rrnequiv  30258  upbdrech2  31408  stoweidlem9  31632  fourierdlem31  31761  raaan2  31970
  Copyright terms: Public domain W3C validator