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

Theorem rabid 2675
Description: An "identity" law of concretion for restricted abstraction. Special case of Definition 2.1 of [Quine] p. 16. (Contributed by NM, 9-Oct-2003.)
Assertion
Ref Expression
rabid  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )

Proof of Theorem rabid
StepHypRef Expression
1 df-rab 2516 . 2  |-  { x  e.  A  |  ph }  =  { x  |  ( x  e.  A  /\  ph ) }
21abeq2i 2356 1  |-  ( x  e.  { x  e.  A  |  ph }  <->  ( x  e.  A  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1621   {crab 2512
This theorem is referenced by:  rabeq2i  2724  reusv2lem4  4429  reusv2  4431  rabxfrd  4446  tfis  4536  riotaxfrd  6222  rankr1ai  7354  cfval2  7770  cflim3  7772  cflim2  7773  cfss  7775  cfslb  7776  cofsmo  7779  nnwos  10165  ramval  12929  ramub1lem1  12947  hauseqlcld  17172  ptcmplem4  17581  mbfinf  18852  itg2monolem1  18937  lhop1  19193  sgplpte21a  25299  cover2  25524  aaitgo  26533  rfcnpre1  26857  rfcnpre2  26869  stoweidlem24  26907  stoweidlem27  26910  stoweidlem31  26914  stoweidlem34  26917  stoweidlem35  26918  stoweidlem54  26937  stoweidlem57  26940  stoweidlem59  26942  bnj1204  27828
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-12o 1664  ax-9 1684  ax-4 1692  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-rab 2516
  Copyright terms: Public domain W3C validator