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

Theorem elrab2 3560
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)
Hypotheses
Ref Expression
elrab2.1 (𝑥 = 𝐴 → (𝜑𝜓))
elrab2.2 𝐶 = {𝑥𝐵𝜑}
Assertion
Ref Expression
elrab2 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem elrab2
StepHypRef Expression
1 elrab2.2 . . 3 𝐶 = {𝑥𝐵𝜑}
21eleq2i 2875 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 3557 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 266 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  {crab 3098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-rab 3103  df-v 3391
This theorem is referenced by:  elrabsf  3670  pwnss  5020  fvmpti  6500  fvmptss2  6523  tfis  7282  elom  7296  oawordeulem  7869  oeeulem  7916  mapfienlem1  8547  mapfienlem3  8549  mapfien  8550  ordtypelem2  8661  ordtypelem3  8662  ordtypelem9  8668  wemapso2lem  8694  inf3lema  8766  oemapvali  8826  tz9.12lem3  8897  cofsmo  9374  enfin2i  9426  fin23lem28  9445  isf32lem6  9463  hsmexlem4  9534  zorn2lem2  9602  pwfseqlem1  9763  pwfseqlem3  9765  nqereu  10034  elz  11643  zsupss  11994  rpnnen1lem5  12035  elrp  12046  repos  12487  wwlktovf  13922  wwlktovf1  13923  wwlktovfo  13924  sqrlem1  14204  sqrlem2  14205  sqrlem6  14209  sqrlem7  14210  ello1  14467  elo1  14478  rlimrege0  14531  divalglem2  15336  divalglem4  15337  divalglem5  15338  divalglem9  15342  divalglem10  15343  bitsfzolem  15373  gcdcllem1  15438  gcdcllem2  15439  gcdcllem3  15440  bezoutlem1  15473  bezoutlem3  15475  bezoutlem4  15476  isprm  15603  maxprmfct  15636  phimullem  15699  eulerthlem1  15701  eulerthlem2  15702  hashgcdlem  15708  pclem  15758  pcprecl  15759  pcprendvds  15760  infpn2  15832  prmreclem1  15835  prmreclem2  15836  prmreclem3  15837  prmreclem5  15839  1arith  15846  elgz  15850  4sqlem13  15876  4sqlem17  15880  4sqlem18  15881  vdwnnlem2  15915  vdwnnlem3  15916  ramtlecl  15919  isdrs  17137  istos  17238  islat  17250  isclat  17312  isdlat  17396  istsr  17420  issgrp  17488  ismnddef  17499  gsumvallem2  17575  isgrp  17631  elnmz  17833  gastacl  17941  gastacos  17942  symgfixelq  18052  psgneldm  18122  sylow1lem2  18213  sylow1lem4  18215  sylow2alem1  18231  sylow2alem2  18232  efgsdm  18342  iscmn  18399  iscyg  18480  iscyggen  18481  dprdw  18609  ablfacrplem  18664  ablfacrp  18665  ablfac1c  18670  ablfac1eu  18672  pgpfaclem1  18680  ablfaclem3  18686  ablfac2  18688  issrg  18707  isring  18751  iscrng  18754  isdrng  18953  islmod  19069  islvec  19309  lspsolvlem  19348  lbsextlem1  19365  lbsextlem3  19367  lbsextlem4  19368  islpir  19456  isnzr  19466  isrrg  19495  isdomn  19501  isassa  19522  psrbag  19571  psrbaglefi  19579  psrbagconcl  19580  psrbagconf1o  19581  gsumbagdiaglem  19582  mplelbas  19637  isphl  20181  pjdm  20259  ishil  20270  frlmssuvc1  20341  frlmssuvc2  20342  frlmsslsp  20343  gsummatr01lem1  20671  gsummatr01lem4  20674  gsummatr01  20675  mretopd  21108  neipeltop  21145  isperf  21167  ist0  21336  ist1  21337  ishaus  21338  iscnrm  21339  isreg  21348  isnrm  21351  ispnrm  21355  iscmp  21403  hauscmplem  21421  isconn  21428  conncompss  21448  is1stc  21456  islly  21483  isnlly  21484  dfac14lem  21632  ishmeo  21774  ptcmplem3  22069  ptcmplem4  22070  istmd  22089  istgp  22092  tgpconncompeqg  22126  tgpt0  22133  qustgpopn  22134  istrg  22178  istdrg  22180  istlm  22199  istvc  22206  iscusp  22314  imasdsf1olem  22389  isxms  22463  isms  22465  blcld  22521  prdsxmslem2  22545  isngp  22611  isnrg  22675  isnlm  22690  icccmplem1  22836  icccmplem2  22837  isclm  23074  iscph  23180  isbn  23345  iscms  23352  ivthlem1  23430  ivthlem2  23431  ivthlem3  23432  elovolm  23454  ovolicc2lem2  23497  ovolicc2lem4  23499  ovolicc2lem5  23500  ismbl  23505  dyadmbllem  23578  dyadmbl  23579  ismbf1  23603  isi1f  23653  isibl  23744  isuc1p  24112  ismon1p  24114  radcnvle  24386  abelthlem2  24398  abelthlem7a  24403  atans  24869  lgamgulmlem2  24968  lgamgulmlem3  24969  lgamgulmlem5  24971  lgambdd  24975  wilthlem2  25007  wilthlem3  25008  ftalem3  25013  sqff1o  25120  dvdsmulf1o  25132  lgslem2  25235  lgslem3  25236  lgsfcl2  25240  rpvmasumlem  25388  dchrvmaeq0  25405  dchrisum0re  25414  pntlem3  25510  axcontlem2  26057  lfgredgge2  26231  uspgredg2vlem  26328  uspgredg2v  26329  usgredg2vlem1  26330  usgredg2vlem2  26331  ushgredgedg  26334  ushgredgedgloop  26336  ushgredgedgloopOLD  26337  uhgrspan1  26409  upgrreslem  26410  umgrreslem  26411  isfusgr  26424  nbupgrres  26479  nbusgredgeu0  26484  nbusgrf1o0  26485  uvtxel  26505  uvtxel1  26515  cusgrexilem2  26564  cusgrfilem2  26578  vtxdginducedm1lem4  26664  iswspthn  26969  wwlknon  26979  wspthnon  26980  wspthnonOLD  26982  wlknwwlksnfunOLD  27013  wlknwwlksninjOLD  27014  wlkwwlkfunOLD  27021  wlkwwlkinjOLD  27022  wlkwwlksurOLD  27023  wwlksnextfun  27033  wwlksnextinj  27034  wwlksnextsur  27035  wwlksnextproplem3  27047  clwlkclwwlkflem  27145  clwlkclwwlkfolem  27148  isclwwlkn  27171  clwwlkel  27193  clwwlkf  27194  clwwlkf1  27196  clwlksfclwwlk1hashnOLD  27231  clwlksfoclwwlkOLD  27235  clwlksf1clwwlklem0OLD  27236  isclwwlknon  27255  frgrwopreglem3  27487  frgrwopreglem5lem  27493  frgrwopreglem5  27494  isablo  27727  iscbn  28046  hcau  28367  issh  28391  isch  28405  elcnop  29042  ellnop  29043  elbdop  29045  elhmop  29058  elcnfn  29067  ellnfn  29068  isst  29398  ishst  29399  ela  29524  isomnd  30024  isslmd  30078  isorng  30122  iscref  30234  isrrext  30367  ispisys  30538  isldsys  30542  isros  30554  issros  30561  oddpwdc  30739  eulerpartleme  30748  eulerpartlemo  30750  eulerpartlemd  30751  eulerpartlemt0  30754  eulerpartlemf  30755  eulerpartlemt  30756  eulerpartlemr  30759  eulerpartlemmf  30760  eulerpartlemgvv  30761  eulerpartlemgs2  30765  eulerpartlemn  30766  elprob  30794  ballotlemelo  30872  ballotleme  30881  bnj1152  31387  bnj1280  31409  subfacp1lem3  31485  subfacp1lem5  31487  erdszelem1  31494  ispconn  31526  issconn  31529  cvmsiota  31580  cvmlift2lem12  31617  rdgprc0  32017  elwlim  32087  neibastop1  32673  neibastop2lem  32674  neibastop2  32675  topdifinffinlem  33509  poimirlem5  33725  poimirlem6  33726  poimirlem7  33727  poimirlem8  33728  poimirlem10  33730  poimirlem11  33731  poimirlem12  33732  poimirlem15  33735  poimirlem16  33736  poimirlem17  33737  poimirlem18  33738  poimirlem19  33739  poimirlem20  33740  poimirlem21  33741  poimirlem22  33742  isprrngo  34158  rabeqel  34335  toycom  34751  isopos  34958  isoml  35016  isatl  35077  iscvlat  35101  ishlat1  35130  cdlemm10N  36897  dihglblem2N  37073  lcfl1lem  37270  lcfls1lem  37313  mapdordlem1a  37413  mapdordlem1  37415  pellqrex  37943  islnm  38146  pwssplit4  38158  islnr  38180  fnlimcnv  40377  stoweidlem14  40708  stoweidlem16  40710  stoweidlem37  40731  stoweidlem48  40742  stoweidlem51  40745  stoweidlem59  40753  salexct  41029  salexct2  41034  salexct3  41037  salgencntex  41038  salgensscntex  41039  ovn0lem  41259  opnvonmbllem1  41326  ovolval5lem2  41347  pimincfltioc  41406  pimdecfgtioo  41407  pimincfltioo  41408  smfresal  41475  smfmullem2  41479  smfpimbor1lem1  41485  smfpimbor1lem2  41486  smfinflem  41503  iseven  42114  isodd  42115  m1expevenALTV  42133  iseven2  42137  isodd3  42138  odd2np1ALTV  42158  opoeALTV  42167  opeoALTV  42168  isgbe  42212  isgbow  42213  isgbo  42214  sprsymrelfo  42313  0nodd  42376  1odd  42377  2nodd  42378  iscmgmALT  42426  issgrpALT  42427  iscsgrpALT  42428  isrng  42442  1neven  42498  2zlidl  42500  2zrngamgm  42505  2zrngagrp  42509  2zrngmmgm  42512  2zrngnmrid  42516
  Copyright terms: Public domain W3C validator