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

Theorem rabeq0 3476
Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.)
Assertion
Ref Expression
rabeq0  |-  ( { x  e.  A  |  ph }  =  (/)  <->  A. x  e.  A  -.  ph )

Proof of Theorem rabeq0
StepHypRef Expression
1 ralnex 2553 . 2  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
2 rabn0 3474 . . 3  |-  ( { x  e.  A  |  ph }  =/=  (/)  <->  E. x  e.  A  ph )
32necon1bbii 2498 . 2  |-  ( -. 
E. x  e.  A  ph  <->  { x  e.  A  |  ph }  =  (/) )
41, 3bitr2i 241 1  |-  ( { x  e.  A  |  ph }  =  (/)  <->  A. x  e.  A  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    = wceq 1623   A.wral 2543   E.wrex 2544   {crab 2547   (/)c0 3455
This theorem is referenced by:  rabnc  3478  dffr2  4358  frc  4359  frirr  4370  wereu2  4390  fndmdifeq0  5631  cantnf  7395  wemapwe  7400  hashbclem  11390  hashbc  11391  smuval2  12673  smupvallem  12674  smu01lem  12676  smumullem  12683  phiprmpw  12844  prmreclem4  12966  efgsfo  15048  00lsp  15738  ordthauslem  17111  pthaus  17332  xkohaus  17347  hmeofval  17449  mumul  20419  musum  20431  ppiub  20443  lgsquadlem2  20594  subfacp1lem6  23127  vdgr1b  23306  vdgr1a  23308  eupath2  23315  tz6.26  23616  areacirclem6  24342  bsstrs  25558  nbssntrs  25559  rabeq0OLD  25763  fnnfpeq0  26170  0dioph  26270  dsmm0cl  26618  hashgcdeq  26929
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-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator