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

Theorem elrab2 3108
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 2497 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3106 . 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 1362    e. wcel 1755   {crab 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714  df-v 2964
This theorem is referenced by:  elrabsf  3213  pwnss  4445  fvmpti  5761  fvmptss2  5781  tfis  6454  elom  6468  oawordeulem  6981  oeeulem  7028  mapfienlem1  7642  mapfienlem3  7644  mapfien  7645  ordtypelem2  7721  ordtypelem3  7722  ordtypelem9  7728  wemapso2OLD  7754  wemapso2lem  7755  inf3lema  7818  oemapvali  7880  mapfienOLD  7915  tz9.12lem3  7984  cofsmo  8426  enfin2i  8478  fin23lem28  8497  isf32lem6  8515  hsmexlem4  8586  zorn2lem2  8654  pwfseqlem1  8812  pwfseqlem3  8814  nqereu  9085  elz  10635  zsupss  10931  rpnnen1lem5  10970  elrp  10980  repos  11373  sqrlem1  12715  sqrlem2  12716  sqrlem6  12720  sqrlem7  12721  ello1  12976  elo1  12987  rlimrege0  13040  divalglem2  13581  divalglem4  13582  divalglem5  13583  divalglem9  13587  divalglem10  13588  bitsfzolem  13612  gcdcllem1  13677  gcdcllem2  13678  gcdcllem3  13679  bezoutlem1  13704  bezoutlem3  13706  bezoutlem4  13707  isprm  13747  maxprmfct  13781  phimullem  13836  eulerthlem1  13838  eulerthlem2  13839  pclem  13887  pcprecl  13888  pcprendvds  13889  infpn2  13956  prmreclem1  13959  prmreclem2  13960  prmreclem3  13961  prmreclem5  13963  1arith  13970  elgz  13974  4sqlem13  14000  4sqlem17  14004  4sqlem18  14005  vdwnnlem2  14039  vdwnnlem3  14040  ramtlecl  14043  isdrs  15086  istos  15187  islat  15199  isclat  15261  isdlat  15345  istsr  15369  gsumvallem2  15482  isgrp  15528  elnmz  15699  gastacl  15806  gastacos  15807  symgfixelq  15917  psgneldm  15988  sylow1lem2  16077  sylow1lem4  16079  sylow2alem1  16095  sylow2alem2  16096  efgsdm  16206  iscmn  16263  iscyg  16335  iscyggen  16336  dprdw  16467  dprdwOLD  16473  ablfacrplem  16539  ablfacrp  16540  ablfac1c  16545  ablfac1eu  16547  pgpfaclem1  16555  ablfaclem3  16561  ablfac2  16563  isrng  16584  iscrng  16587  isdrng  16759  islmod  16875  islvec  17106  lspsolvlem  17144  lbsextlem1  17160  lbsextlem3  17162  lbsextlem4  17163  islpir  17252  isnzr  17262  isrrg  17280  isdomn  17287  isassa  17308  psrbag  17364  psrbaglefi  17374  psrbaglefiOLD  17375  psrbagconcl  17376  psrbagconf1o  17377  gsumbagdiaglem  17378  mplelbas  17437  mplelbasOLD  17439  isphl  17898  pjdm  17973  ishil  17984  frlmssuvc1  18060  frlmssuvc2  18061  frlmssuvc1OLD  18062  frlmssuvc2OLD  18063  frlmsslsp  18064  frlmsslspOLD  18065  gsummatr01lem1  18302  gsummatr01lem4  18305  gsummatr01  18306  mretopd  18537  neipeltop  18574  isperf  18596  ist0  18765  ist1  18766  ishaus  18767  iscnrm  18768  isreg  18777  isnrm  18780  ispnrm  18784  iscmp  18832  hauscmplem  18850  iscon  18858  concompss  18878  is1stc  18886  islly  18913  isnlly  18914  dfac14lem  19031  ishmeo  19173  ptcmplem3  19467  ptcmplem4  19468  istmd  19486  istgp  19489  tgpconcompeqg  19523  tgpt0  19530  divstgpopn  19531  istrg  19579  istdrg  19581  istlm  19600  istvc  19607  iscusp  19715  imasdsf1olem  19789  isxms  19863  isms  19865  blcld  19921  prdsxmslem2  19945  isngp  20029  isnrg  20082  isnlm  20097  icccmplem1  20240  icccmplem2  20241  isclm  20477  iscph  20530  isbn  20690  iscms  20697  ivthlem1  20776  ivthlem2  20777  ivthlem3  20778  elovolm  20799  ovolicc2lem2  20842  ovolicc2lem4  20844  ovolicc2lem5  20845  ismbl  20850  dyadmbllem  20920  dyadmbl  20921  ismbf1  20945  isi1f  20993  isibl  21084  isuc1p  21496  ismon1p  21498  radcnvle  21769  abelthlem2  21781  abelthlem7a  21786  atans  22209  wilthlem2  22291  wilthlem3  22292  ftalem3  22296  sqff1o  22404  dvdsmulf1o  22418  lgslem2  22520  lgslem3  22521  lgsfcl2  22525  rpvmasumlem  22620  dchrvmaeq0  22637  dchrisum0re  22646  pntlem3  22742  axcontlem2  23033  usgraidx2vlem1  23131  usgraidx2vlem2  23132  cusgraexi  23198  cusgrafilem2  23210  isablo  23592  iscbn  24087  hcau  24408  issh  24432  isch  24447  elcnop  25083  ellnop  25084  elbdop  25086  elhmop  25099  elcnfn  25108  ellnfn  25109  isst  25439  ishst  25440  ela  25565  isomnd  25987  isarchi  26022  issrg  26041  isslmd  26066  isorng  26119  isrrext  26282  oddpwdc  26584  eulerpartleme  26593  eulerpartlemo  26595  eulerpartlemd  26596  eulerpartlemt0  26599  eulerpartlemf  26600  eulerpartlemt  26601  eulerpartlemr  26604  eulerpartlemmf  26605  eulerpartlemgvv  26606  eulerpartlemgs2  26610  eulerpartlemn  26611  elprob  26639  ballotlemelo  26717  ballotleme  26726  lgamgulmlem2  26863  lgamgulmlem3  26864  lgamgulmlem5  26866  lgambdd  26870  subfacp1lem3  26917  subfacp1lem5  26919  erdszelem1  26926  ispcon  26959  isscon  26962  cvmsiota  27013  cvmlift2lem12  27050  rdgprc0  27453  elwlim  27606  neibastop1  28421  neibastop2lem  28422  neibastop2  28423  isprrngo  28691  pellqrex  29062  islnm  29272  pwssplit4  29284  islnr  29309  hashgcdlem  29407  stoweidlem14  29652  stoweidlem16  29654  stoweidlem37  29675  stoweidlem48  29686  stoweidlem51  29689  stoweidlem59  29697  wlknwwlknfun  30185  wlknwwlkninj  30186  wlkiswwlkfun  30192  wlkiswwlkinj  30193  wwlkextfun  30204  clwwlkel  30298  clwwlkf  30299  clwwlkf1  30301  clwlkfoclwwlk  30361  clwlkf1clwwlklem3  30364  wwlkextproplem3  30405  frgrawopreglem3  30482  extwwlkfab  30526  bnj1152  31688  bnj1280  31710  toycom  32188  isopos  32395  isoml  32453  isatl  32514  iscvlat  32538  ishlat1  32567  cdlemm10N  34333  dihglblem2N  34509  lcfl1lem  34706  lcfls1lem  34749  mapdordlem1a  34849  mapdordlem1  34851
  Copyright terms: Public domain W3C validator