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

Theorem elrab2 2925
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
Hypotheses
Ref Expression
elrab2.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
elrab2.2  |-  C  =  { x  e.  B  |  ph }
Assertion
Ref Expression
elrab2  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hints:    ph( x)    C( x)

Proof of Theorem elrab2
StepHypRef Expression
1 elrab2.2 . . 3  |-  C  =  { x  e.  B  |  ph }
21eleq2i 2347 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 2923 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 240 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   {crab 2547
This theorem is referenced by:  elrabsf  3029  pwnss  4176  tfis  4645  elom  4659  fvmpti  5601  fvmptss2  5619  oawordeulem  6552  oeeulem  6599  ordtypelem2  7234  ordtypelem3  7235  ordtypelem9  7241  wemapso2  7267  inf3lema  7325  oemapvali  7386  mapfien  7399  tz9.12lem3  7461  cofsmo  7895  enfin2i  7947  fin23lem28  7966  isf32lem6  7984  hsmexlem4  8055  zorn2lem2  8124  pwfseqlem1  8280  pwfseqlem3  8282  nqereu  8553  elz  10026  zsupss  10307  rpnnen1lem5  10346  elrp  10356  repos  10740  sqrlem1  11728  sqrlem2  11729  sqrlem6  11733  sqrlem7  11734  ello1  11989  elo1  12000  rlimrege0  12053  divalglem2  12594  divalglem4  12595  divalglem5  12596  divalglem9  12600  divalglem10  12601  bitsfzolem  12625  gcdcllem1  12690  gcdcllem2  12691  gcdcllem3  12692  bezoutlem1  12717  bezoutlem3  12719  bezoutlem4  12720  isprm  12760  maxprmfct  12792  phimullem  12847  eulerthlem1  12849  eulerthlem2  12850  pclem  12891  pcprecl  12892  pcprendvds  12893  infpn2  12960  prmreclem1  12963  prmreclem2  12964  prmreclem3  12965  prmreclem5  12967  1arith  12974  elgz  12978  4sqlem13  13004  4sqlem17  13008  4sqlem18  13009  vdwnnlem2  13043  vdwnnlem3  13044  ramtlecl  13047  isdrs  14068  istos  14141  islat  14153  isclat  14215  isdlat  14296  istsr  14326  isla  14342  gsumvallem2  14449  isgrp  14493  elnmz  14656  gastacl  14763  gastacos  14764  sylow1lem2  14910  sylow1lem4  14912  sylow2alem1  14928  sylow2alem2  14929  efgsdm  15039  iscmn  15096  iscyg  15166  iscyggen  15167  dprdw  15245  ablfacrplem  15300  ablfacrp  15301  ablfac1c  15306  ablfac1eu  15308  pgpfaclem1  15316  ablfaclem3  15322  ablfac2  15324  isrng  15345  iscrng  15348  isdrng  15516  islmod  15631  islvec  15857  lspsolvlem  15895  lbsextlem1  15911  lbsextlem3  15913  lbsextlem4  15914  islpir  16001  isnzr  16011  isrrg  16029  isdomn  16035  isassa  16056  psrbag  16112  psrbaglefi  16118  psrbagconcl  16119  psrbagconf1o  16120  gsumbagdiaglem  16121  mplelbas  16175  isphl  16532  pjdm  16607  ishil  16618  mretopd  16829  isperf  16882  ist0  17048  ist1  17049  ishaus  17050  iscnrm  17051  isreg  17060  isnrm  17063  ispnrm  17067  iscmp  17115  hauscmplem  17133  iscon  17139  concompss  17159  is1stc  17167  islly  17194  isnlly  17195  dfac14lem  17311  ishmeo  17450  ptcmplem3  17748  ptcmplem4  17749  istmd  17757  istgp  17760  tgpconcompeqg  17794  tgpt0  17801  divstgpopn  17802  istrg  17846  istdrg  17848  istlm  17867  istvc  17874  imasdsf1olem  17937  isxms  17993  isms  17995  blcld  18051  prdsxmslem2  18075  isngp  18118  isnrg  18171  isnlm  18186  icccmplem1  18327  icccmplem2  18328  isclm  18562  iscph  18606  isbn  18760  iscms  18767  ivthlem1  18811  ivthlem2  18812  ivthlem3  18813  elovolm  18834  ovolicc2lem2  18877  ovolicc2lem4  18879  ovolicc2lem5  18880  ismbl  18885  dyadmbllem  18954  dyadmbl  18955  ismbf1  18981  isi1f  19029  isibl  19120  isuc1p  19526  ismon1p  19528  radcnvle  19796  abelthlem2  19808  abelthlem7a  19813  atans  20226  wilthlem2  20307  wilthlem3  20308  ftalem3  20312  sqff1o  20420  dvdsmulf1o  20434  lgslem2  20536  lgslem3  20537  lgsfcl2  20541  rpvmasumlem  20636  dchrvmaeq0  20653  dchrisum0re  20662  pntlem3  20758  isablo  20950  iscbn  21443  hcau  21763  issh  21787  isch  21802  elcnop  22437  ellnop  22438  elbdop  22440  elhmop  22453  elcnfn  22462  ellnfn  22463  isst  22793  ishst  22794  ela  22919  ballotlemelo  23046  ballotleme  23055  elprob  23612  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem1  23722  ispcon  23754  isscon  23757  cvmsiota  23808  cvmlift2lem12  23845  rdgprc0  24150  axcontlem2  24593  isibg2  26110  neibastop1  26308  neibastop2lem  26309  neibastop2  26310  isprrngo  26675  pellqrex  26964  islnm  27175  pwssplit4  27191  frlmssuvc1  27246  frlmssuvc2  27247  frlmsslsp  27248  islnr  27315  psgneldm  27426  hashgcdlem  27516  stoweidlem16  27765  stoweidlem48  27797  stoweidlem51  27800  stoweidlem59  27808  bnj1152  29028  bnj1280  29050  toycom  29162  isopos  29370  isoml  29428  isatl  29489  iscvlat  29513  ishlat1  29542  cdlemm10N  31308  dihglblem2N  31484  lcfl1lem  31681  lcfls1lem  31724  mapdordlem1a  31824  mapdordlem1  31826
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-rab 2552  df-v 2790
  Copyright terms: Public domain W3C validator