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

Theorem elrab2 3332
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 2679 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 3330 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 262 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  {crab 2899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174
This theorem is referenced by:  elrabsf  3440  pwnss  4751  fvmpti  6175  fvmptss2  6197  tfis  6923  elom  6937  oawordeulem  7498  oeeulem  7545  mapfienlem1  8170  mapfienlem3  8172  mapfien  8173  ordtypelem2  8284  ordtypelem3  8285  ordtypelem9  8291  wemapso2lem  8317  inf3lema  8381  oemapvali  8441  tz9.12lem3  8512  cofsmo  8951  enfin2i  9003  fin23lem28  9022  isf32lem6  9040  hsmexlem4  9111  zorn2lem2  9179  pwfseqlem1  9336  pwfseqlem3  9338  nqereu  9607  elz  11212  zsupss  11609  rpnnen1lem5  11650  rpnnen1lem5OLD  11656  elrp  11666  repos  12097  wwlktovf  13493  wwlktovf1  13494  wwlktovfo  13495  sqrlem1  13777  sqrlem2  13778  sqrlem6  13782  sqrlem7  13783  ello1  14040  elo1  14051  rlimrege0  14104  divalglem2  14902  divalglem4  14903  divalglem5  14904  divalglem9  14908  divalglem10  14909  bitsfzolem  14940  gcdcllem1  15005  gcdcllem2  15006  gcdcllem3  15007  bezoutlem1  15040  bezoutlem3  15042  bezoutlem4  15043  isprm  15171  maxprmfct  15205  phimullem  15268  eulerthlem1  15270  eulerthlem2  15271  hashgcdlem  15277  pclem  15327  pcprecl  15328  pcprendvds  15329  infpn2  15401  prmreclem1  15404  prmreclem2  15405  prmreclem3  15406  prmreclem5  15408  1arith  15415  elgz  15419  4sqlem13  15445  4sqlem17  15449  4sqlem18  15450  vdwnnlem2  15484  vdwnnlem3  15485  ramtlecl  15488  isdrs  16703  istos  16804  islat  16816  isclat  16878  isdlat  16962  istsr  16986  issgrp  17054  ismnddef  17065  gsumvallem2  17141  isgrp  17197  elnmz  17402  gastacl  17511  gastacos  17512  symgfixelq  17622  psgneldm  17692  sylow1lem2  17783  sylow1lem4  17785  sylow2alem1  17801  sylow2alem2  17802  efgsdm  17912  iscmn  17969  iscyg  18050  iscyggen  18051  dprdw  18178  ablfacrplem  18233  ablfacrp  18234  ablfac1c  18239  ablfac1eu  18241  pgpfaclem1  18249  ablfaclem3  18255  ablfac2  18257  issrg  18276  isring  18320  iscrng  18323  isdrng  18520  islmod  18636  islvec  18871  lspsolvlem  18909  lbsextlem1  18925  lbsextlem3  18927  lbsextlem4  18928  islpir  19016  isnzr  19026  isrrg  19055  isdomn  19061  isassa  19082  psrbag  19131  psrbaglefi  19139  psrbagconcl  19140  psrbagconf1o  19141  gsumbagdiaglem  19142  mplelbas  19197  isphl  19737  pjdm  19812  ishil  19823  frlmssuvc1  19894  frlmssuvc2  19895  frlmsslsp  19896  gsummatr01lem1  20222  gsummatr01lem4  20225  gsummatr01  20226  mretopd  20648  neipeltop  20685  isperf  20707  ist0  20876  ist1  20877  ishaus  20878  iscnrm  20879  isreg  20888  isnrm  20891  ispnrm  20895  iscmp  20943  hauscmplem  20961  iscon  20968  concompss  20988  is1stc  20996  islly  21023  isnlly  21024  dfac14lem  21172  ishmeo  21314  ptcmplem3  21610  ptcmplem4  21611  istmd  21630  istgp  21633  tgpconcompeqg  21667  tgpt0  21674  qustgpopn  21675  istrg  21719  istdrg  21721  istlm  21740  istvc  21747  iscusp  21855  imasdsf1olem  21929  isxms  22003  isms  22005  blcld  22061  prdsxmslem2  22085  isngp  22151  isnrg  22207  isnlm  22222  icccmplem1  22365  icccmplem2  22366  isclm  22603  iscph  22702  isbn  22860  iscms  22867  ivthlem1  22944  ivthlem2  22945  ivthlem3  22946  elovolm  22967  ovolicc2lem2  23010  ovolicc2lem4  23012  ovolicc2lem5  23013  ismbl  23018  dyadmbllem  23090  dyadmbl  23091  ismbf1  23116  isi1f  23164  isibl  23255  isuc1p  23621  ismon1p  23623  radcnvle  23895  abelthlem2  23907  abelthlem7a  23912  atans  24374  lgamgulmlem2  24473  lgamgulmlem3  24474  lgamgulmlem5  24476  lgambdd  24480  wilthlem2  24512  wilthlem3  24513  ftalem3  24518  sqff1o  24625  dvdsmulf1o  24637  lgslem2  24740  lgslem3  24741  lgsfcl2  24745  rpvmasumlem  24893  dchrvmaeq0  24910  dchrisum0re  24919  pntlem3  25015  axcontlem2  25563  usgraidx2vlem1  25686  usgraidx2vlem2  25687  cusgraexi  25763  cusgrafilem2  25774  wlknwwlknfun  26004  wlknwwlkninj  26005  wlkiswwlkfun  26011  wlkiswwlkinj  26012  wlkiswwlksur  26013  wwlkextfun  26023  wwlkextinj  26024  wwlkextsur  26025  wwlkextproplem3  26037  clwwlkel  26087  clwwlkf  26088  clwwlkf1  26090  clwlkfclwwlk1hashn  26134  clwlkfoclwwlk  26138  clwlkf1clwwlklem1  26139  clwlkf1clwwlklem2  26140  clwlkf1clwwlklem3  26141  frgrawopreglem3  26339  extwwlkfab  26383  isablo  26553  iscbn  26910  hcau  27231  issh  27255  isch  27269  elcnop  27906  ellnop  27907  elbdop  27909  elhmop  27922  elcnfn  27931  ellnfn  27932  isst  28262  ishst  28263  ela  28388  isomnd  28838  isslmd  28892  isorng  28936  iscref  29045  isrrext  29178  ispisys  29348  isldsys  29352  isros  29364  issros  29371  oddpwdc  29549  eulerpartleme  29558  eulerpartlemo  29560  eulerpartlemd  29561  eulerpartlemt0  29564  eulerpartlemf  29565  eulerpartlemt  29566  eulerpartlemr  29569  eulerpartlemmf  29570  eulerpartlemgvv  29571  eulerpartlemgs2  29575  eulerpartlemn  29576  elprob  29604  ballotlemelo  29682  ballotleme  29691  bnj1152  30126  bnj1280  30148  subfacp1lem3  30224  subfacp1lem5  30226  erdszelem1  30233  ispcon  30265  isscon  30268  cvmsiota  30319  cvmlift2lem12  30356  rdgprc0  30749  elwlim  30819  elwlimOLD  30820  neibastop1  31330  neibastop2lem  31331  neibastop2  31332  topdifinffinlem  32167  poimirlem5  32380  poimirlem6  32381  poimirlem7  32382  poimirlem8  32383  poimirlem10  32385  poimirlem11  32386  poimirlem12  32387  poimirlem15  32390  poimirlem16  32391  poimirlem17  32392  poimirlem18  32393  poimirlem19  32394  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  isprrngo  32815  toycom  33074  isopos  33281  isoml  33339  isatl  33400  iscvlat  33424  ishlat1  33453  cdlemm10N  35221  dihglblem2N  35397  lcfl1lem  35594  lcfls1lem  35637  mapdordlem1a  35737  mapdordlem1  35739  pellqrex  36257  islnm  36461  pwssplit4  36473  islnr  36496  fnlimcnv  38531  stoweidlem14  38704  stoweidlem16  38706  stoweidlem37  38727  stoweidlem48  38738  stoweidlem51  38741  stoweidlem59  38749  salexct  39025  salexct2  39030  salexct3  39033  salgencntex  39034  salgensscntex  39035  ovn0lem  39252  opnvonmbllem1  39319  ovolval5lem2  39340  pimincfltioc  39400  pimdecfgtioo  39401  pimincfltioo  39402  smfresal  39470  smfmullem2  39474  smfpimbor1lem1  39480  smfpimbor1lem2  39481  m1expevenALTV  39896  iseven2  39900  isodd3  39901  odd2np1ALTV  39921  opoeALTV  39930  opeoALTV  39931  isgbe  39971  isgbo  39972  isgboa  39973  lfgredgge2  40344  uspgredg2vlem  40445  uspgredg2v  40446  usgredg2vlem1  40447  usgredg2vlem2  40448  ushgredgedga  40451  ushgredgedgaloop  40453  uhgrspan1  40522  isfusgr  40532  nbupgrres  40587  iscusgr  40635  cusgrexi  40657  cusgrfilem2  40667  iswspthn  41042  wlknwwlksnfun  41080  wlknwwlksninj  41081  wlkwwlkfun  41087  wlkwwlkinj  41088  wlkwwlksur  41089  wwlksnextfun  41099  wwlksnextinj  41100  wwlksnextsur  41101  wwlksnextproplem3  41112  clwwlksel  41216  clwwlksf  41217  clwwlksf1  41219  clwlksfclwwlk1hashn  41261  clwlksfoclwwlk  41265  clwlksf1clwwlklem0  41266  frgrwopreglem3  41478  av-extwwlkfab  41515  0nodd  41595  1odd  41596  2nodd  41597  iscmgmALT  41645  issgrpALT  41646  iscsgrpALT  41647  isrng  41661  1neven  41717  2zlidl  41719  2zrngamgm  41724  2zrngagrp  41728  2zrngmmgm  41731  2zrngnmrid  41735
  Copyright terms: Public domain W3C validator