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

Theorem elrab2 3140
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 2507 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3138 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 249 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   {crab 2740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995
This theorem is referenced by:  elrabsf  3246  pwnss  4478  fvmpti  5794  fvmptss2  5814  tfis  6486  elom  6500  oawordeulem  7014  oeeulem  7061  mapfienlem1  7675  mapfienlem3  7677  mapfien  7678  ordtypelem2  7754  ordtypelem3  7755  ordtypelem9  7761  wemapso2OLD  7787  wemapso2lem  7788  inf3lema  7851  oemapvali  7913  mapfienOLD  7948  tz9.12lem3  8017  cofsmo  8459  enfin2i  8511  fin23lem28  8530  isf32lem6  8548  hsmexlem4  8619  zorn2lem2  8687  pwfseqlem1  8846  pwfseqlem3  8848  nqereu  9119  elz  10669  zsupss  10965  rpnnen1lem5  11004  elrp  11014  repos  11407  sqrlem1  12753  sqrlem2  12754  sqrlem6  12758  sqrlem7  12759  ello1  13014  elo1  13025  rlimrege0  13078  divalglem2  13620  divalglem4  13621  divalglem5  13622  divalglem9  13626  divalglem10  13627  bitsfzolem  13651  gcdcllem1  13716  gcdcllem2  13717  gcdcllem3  13718  bezoutlem1  13743  bezoutlem3  13745  bezoutlem4  13746  isprm  13786  maxprmfct  13820  phimullem  13875  eulerthlem1  13877  eulerthlem2  13878  pclem  13926  pcprecl  13927  pcprendvds  13928  infpn2  13995  prmreclem1  13998  prmreclem2  13999  prmreclem3  14000  prmreclem5  14002  1arith  14009  elgz  14013  4sqlem13  14039  4sqlem17  14043  4sqlem18  14044  vdwnnlem2  14078  vdwnnlem3  14079  ramtlecl  14082  isdrs  15125  istos  15226  islat  15238  isclat  15300  isdlat  15384  istsr  15408  gsumvallem2  15522  isgrp  15570  elnmz  15741  gastacl  15848  gastacos  15849  symgfixelq  15959  psgneldm  16030  sylow1lem2  16119  sylow1lem4  16121  sylow2alem1  16137  sylow2alem2  16138  efgsdm  16248  iscmn  16305  iscyg  16377  iscyggen  16378  dprdw  16516  dprdwOLD  16522  ablfacrplem  16588  ablfacrp  16589  ablfac1c  16594  ablfac1eu  16596  pgpfaclem1  16604  ablfaclem3  16610  ablfac2  16612  issrg  16631  isrng  16671  iscrng  16674  isdrng  16858  islmod  16974  islvec  17207  lspsolvlem  17245  lbsextlem1  17261  lbsextlem3  17263  lbsextlem4  17264  islpir  17353  isnzr  17363  isrrg  17381  isdomn  17388  isassa  17409  psrbag  17453  psrbaglefi  17463  psrbaglefiOLD  17464  psrbagconcl  17465  psrbagconf1o  17466  gsumbagdiaglem  17467  mplelbas  17526  mplelbasOLD  17528  isphl  18079  pjdm  18154  ishil  18165  frlmssuvc1  18241  frlmssuvc2  18242  frlmssuvc1OLD  18243  frlmssuvc2OLD  18244  frlmsslsp  18245  frlmsslspOLD  18246  gsummatr01lem1  18483  gsummatr01lem4  18486  gsummatr01  18487  mretopd  18718  neipeltop  18755  isperf  18777  ist0  18946  ist1  18947  ishaus  18948  iscnrm  18949  isreg  18958  isnrm  18961  ispnrm  18965  iscmp  19013  hauscmplem  19031  iscon  19039  concompss  19059  is1stc  19067  islly  19094  isnlly  19095  dfac14lem  19212  ishmeo  19354  ptcmplem3  19648  ptcmplem4  19649  istmd  19667  istgp  19670  tgpconcompeqg  19704  tgpt0  19711  divstgpopn  19712  istrg  19760  istdrg  19762  istlm  19781  istvc  19788  iscusp  19896  imasdsf1olem  19970  isxms  20044  isms  20046  blcld  20102  prdsxmslem2  20126  isngp  20210  isnrg  20263  isnlm  20278  icccmplem1  20421  icccmplem2  20422  isclm  20658  iscph  20711  isbn  20871  iscms  20878  ivthlem1  20957  ivthlem2  20958  ivthlem3  20959  elovolm  20980  ovolicc2lem2  21023  ovolicc2lem4  21025  ovolicc2lem5  21026  ismbl  21031  dyadmbllem  21101  dyadmbl  21102  ismbf1  21126  isi1f  21174  isibl  21265  isuc1p  21634  ismon1p  21636  radcnvle  21907  abelthlem2  21919  abelthlem7a  21924  atans  22347  wilthlem2  22429  wilthlem3  22430  ftalem3  22434  sqff1o  22542  dvdsmulf1o  22556  lgslem2  22658  lgslem3  22659  lgsfcl2  22663  rpvmasumlem  22758  dchrvmaeq0  22775  dchrisum0re  22784  pntlem3  22880  axcontlem2  23233  usgraidx2vlem1  23331  usgraidx2vlem2  23332  cusgraexi  23398  cusgrafilem2  23410  isablo  23792  iscbn  24287  hcau  24608  issh  24632  isch  24647  elcnop  25283  ellnop  25284  elbdop  25286  elhmop  25299  elcnfn  25308  ellnfn  25309  isst  25639  ishst  25640  ela  25765  isomnd  26186  isarchi  26221  isslmd  26240  isorng  26289  isrrext  26451  oddpwdc  26759  eulerpartleme  26768  eulerpartlemo  26770  eulerpartlemd  26771  eulerpartlemt0  26774  eulerpartlemf  26775  eulerpartlemt  26776  eulerpartlemr  26779  eulerpartlemmf  26780  eulerpartlemgvv  26781  eulerpartlemgs2  26785  eulerpartlemn  26786  elprob  26814  ballotlemelo  26892  ballotleme  26901  lgamgulmlem2  27038  lgamgulmlem3  27039  lgamgulmlem5  27041  lgambdd  27045  subfacp1lem3  27092  subfacp1lem5  27094  erdszelem1  27101  ispcon  27134  isscon  27137  cvmsiota  27188  cvmlift2lem12  27225  rdgprc0  27629  elwlim  27782  neibastop1  28606  neibastop2lem  28607  neibastop2  28608  isprrngo  28876  pellqrex  29246  islnm  29456  pwssplit4  29468  islnr  29493  hashgcdlem  29591  stoweidlem14  29835  stoweidlem16  29837  stoweidlem37  29858  stoweidlem48  29869  stoweidlem51  29872  stoweidlem59  29880  wlknwwlknfun  30368  wlknwwlkninj  30369  wlkiswwlkfun  30375  wlkiswwlkinj  30376  wwlkextfun  30387  clwwlkel  30481  clwwlkf  30482  clwwlkf1  30484  clwlkfoclwwlk  30544  clwlkf1clwwlklem3  30547  wwlkextproplem3  30588  frgrawopreglem3  30665  extwwlkfab  30709  dmatid  30913  scmatid  30921  scmatsubcl  30923  bnj1152  32085  bnj1280  32107  toycom  32714  isopos  32921  isoml  32979  isatl  33040  iscvlat  33064  ishlat1  33093  cdlemm10N  34859  dihglblem2N  35035  lcfl1lem  35232  lcfls1lem  35275  mapdordlem1a  35375  mapdordlem1  35377
  Copyright terms: Public domain W3C validator