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

Theorem elrab2 3360
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 2691 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 3357 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 264 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  {crab 2913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197
This theorem is referenced by:  elrabsf  3468  pwnss  4821  fvmpti  6268  fvmptss2  6290  tfis  7039  elom  7053  oawordeulem  7619  oeeulem  7666  mapfienlem1  8295  mapfienlem3  8297  mapfien  8298  ordtypelem2  8409  ordtypelem3  8410  ordtypelem9  8416  wemapso2lem  8442  inf3lema  8506  oemapvali  8566  tz9.12lem3  8637  cofsmo  9076  enfin2i  9128  fin23lem28  9147  isf32lem6  9165  hsmexlem4  9236  zorn2lem2  9304  pwfseqlem1  9465  pwfseqlem3  9467  nqereu  9736  elz  11364  zsupss  11762  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  elrp  11819  repos  12255  wwlktovf  13680  wwlktovf1  13681  wwlktovfo  13682  sqrlem1  13964  sqrlem2  13965  sqrlem6  13969  sqrlem7  13970  ello1  14227  elo1  14238  rlimrege0  14291  divalglem2  15099  divalglem4  15100  divalglem5  15101  divalglem9  15105  divalglem10  15106  bitsfzolem  15137  gcdcllem1  15202  gcdcllem2  15203  gcdcllem3  15204  bezoutlem1  15237  bezoutlem3  15239  bezoutlem4  15240  isprm  15368  maxprmfct  15402  phimullem  15465  eulerthlem1  15467  eulerthlem2  15468  hashgcdlem  15474  pclem  15524  pcprecl  15525  pcprendvds  15526  infpn2  15598  prmreclem1  15601  prmreclem2  15602  prmreclem3  15603  prmreclem5  15605  1arith  15612  elgz  15616  4sqlem13  15642  4sqlem17  15646  4sqlem18  15647  vdwnnlem2  15681  vdwnnlem3  15682  ramtlecl  15685  isdrs  16915  istos  17016  islat  17028  isclat  17090  isdlat  17174  istsr  17198  issgrp  17266  ismnddef  17277  gsumvallem2  17353  isgrp  17409  elnmz  17614  gastacl  17723  gastacos  17724  symgfixelq  17834  psgneldm  17904  sylow1lem2  17995  sylow1lem4  17997  sylow2alem1  18013  sylow2alem2  18014  efgsdm  18124  iscmn  18181  iscyg  18262  iscyggen  18263  dprdw  18390  ablfacrplem  18445  ablfacrp  18446  ablfac1c  18451  ablfac1eu  18453  pgpfaclem1  18461  ablfaclem3  18467  ablfac2  18469  issrg  18488  isring  18532  iscrng  18535  isdrng  18732  islmod  18848  islvec  19085  lspsolvlem  19123  lbsextlem1  19139  lbsextlem3  19141  lbsextlem4  19142  islpir  19230  isnzr  19240  isrrg  19269  isdomn  19275  isassa  19296  psrbag  19345  psrbaglefi  19353  psrbagconcl  19354  psrbagconf1o  19355  gsumbagdiaglem  19356  mplelbas  19411  isphl  19954  pjdm  20032  ishil  20043  frlmssuvc1  20114  frlmssuvc2  20115  frlmsslsp  20116  gsummatr01lem1  20442  gsummatr01lem4  20445  gsummatr01  20446  mretopd  20877  neipeltop  20914  isperf  20936  ist0  21105  ist1  21106  ishaus  21107  iscnrm  21108  isreg  21117  isnrm  21120  ispnrm  21124  iscmp  21172  hauscmplem  21190  isconn  21197  conncompss  21217  is1stc  21225  islly  21252  isnlly  21253  dfac14lem  21401  ishmeo  21543  ptcmplem3  21839  ptcmplem4  21840  istmd  21859  istgp  21862  tgpconncompeqg  21896  tgpt0  21903  qustgpopn  21904  istrg  21948  istdrg  21950  istlm  21969  istvc  21976  iscusp  22084  imasdsf1olem  22159  isxms  22233  isms  22235  blcld  22291  prdsxmslem2  22315  isngp  22381  isnrg  22445  isnlm  22460  icccmplem1  22606  icccmplem2  22607  isclm  22845  iscph  22951  isbn  23116  iscms  23123  ivthlem1  23201  ivthlem2  23202  ivthlem3  23203  elovolm  23224  ovolicc2lem2  23267  ovolicc2lem4  23269  ovolicc2lem5  23270  ismbl  23275  dyadmbllem  23348  dyadmbl  23349  ismbf1  23374  isi1f  23422  isibl  23513  isuc1p  23881  ismon1p  23883  radcnvle  24155  abelthlem2  24167  abelthlem7a  24172  atans  24638  lgamgulmlem2  24737  lgamgulmlem3  24738  lgamgulmlem5  24740  lgambdd  24744  wilthlem2  24776  wilthlem3  24777  ftalem3  24782  sqff1o  24889  dvdsmulf1o  24901  lgslem2  25004  lgslem3  25005  lgsfcl2  25009  rpvmasumlem  25157  dchrvmaeq0  25174  dchrisum0re  25183  pntlem3  25279  axcontlem2  25826  lfgredgge2  26000  uspgredg2vlem  26096  uspgredg2v  26097  usgredg2vlem1  26098  usgredg2vlem2  26099  ushgredgedg  26102  ushgredgedgloop  26104  uhgrspan1  26176  upgrreslem  26177  umgrreslem  26178  isfusgr  26191  nbupgrres  26247  iscusgr  26295  cusgrexilem2  26319  cusgrfilem2  26333  vtxdginducedm1lem4  26419  iswspthn  26717  wlknwwlksnfun  26755  wlknwwlksninj  26756  wlkwwlkfun  26762  wlkwwlkinj  26763  wlkwwlksur  26764  wwlksnextfun  26774  wwlksnextinj  26775  wwlksnextsur  26776  wwlksnextproplem3  26787  clwwlksel  26894  clwwlksf  26895  clwwlksf1  26897  clwlksfclwwlk1hashn  26939  clwlksfoclwwlk  26943  clwlksf1clwwlklem0  26944  frgrwopreglem3  27156  extwwlkfab  27194  isablo  27370  iscbn  27690  hcau  28011  issh  28035  isch  28049  elcnop  28686  ellnop  28687  elbdop  28689  elhmop  28702  elcnfn  28711  ellnfn  28712  isst  29042  ishst  29043  ela  29168  isomnd  29675  isslmd  29729  isorng  29773  iscref  29885  isrrext  30018  ispisys  30189  isldsys  30193  isros  30205  issros  30212  oddpwdc  30390  eulerpartleme  30399  eulerpartlemo  30401  eulerpartlemd  30402  eulerpartlemt0  30405  eulerpartlemf  30406  eulerpartlemt  30407  eulerpartlemr  30410  eulerpartlemmf  30411  eulerpartlemgvv  30412  eulerpartlemgs2  30416  eulerpartlemn  30417  elprob  30445  ballotlemelo  30523  ballotleme  30532  bnj1152  31040  bnj1280  31062  subfacp1lem3  31138  subfacp1lem5  31140  erdszelem1  31147  ispconn  31179  issconn  31182  cvmsiota  31233  cvmlift2lem12  31270  rdgprc0  31673  elwlim  31743  elwlimOLD  31744  neibastop1  32329  neibastop2lem  32330  neibastop2  32331  topdifinffinlem  33166  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem15  33395  poimirlem16  33396  poimirlem17  33397  poimirlem18  33398  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  isprrngo  33820  toycom  34079  isopos  34286  isoml  34344  isatl  34405  iscvlat  34429  ishlat1  34458  cdlemm10N  36226  dihglblem2N  36402  lcfl1lem  36599  lcfls1lem  36642  mapdordlem1a  36742  mapdordlem1  36744  pellqrex  37262  islnm  37466  pwssplit4  37478  islnr  37500  fnlimcnv  39699  stoweidlem14  39994  stoweidlem16  39996  stoweidlem37  40017  stoweidlem48  40028  stoweidlem51  40031  stoweidlem59  40039  salexct  40315  salexct2  40320  salexct3  40323  salgencntex  40324  salgensscntex  40325  ovn0lem  40542  opnvonmbllem1  40609  ovolval5lem2  40630  pimincfltioc  40689  pimdecfgtioo  40690  pimincfltioo  40691  smfresal  40758  smfmullem2  40762  smfpimbor1lem1  40768  smfpimbor1lem2  40769  smfinflem  40786  iseven  41306  isodd  41307  m1expevenALTV  41325  iseven2  41329  isodd3  41330  odd2np1ALTV  41350  opoeALTV  41359  opeoALTV  41360  isgbe  41404  isgbow  41405  isgbo  41406  sprsymrelfo  41512  0nodd  41575  1odd  41576  2nodd  41577  iscmgmALT  41625  issgrpALT  41626  iscsgrpALT  41627  isrng  41641  1neven  41697  2zlidl  41699  2zrngamgm  41704  2zrngagrp  41708  2zrngmmgm  41711  2zrngnmrid  41715
  Copyright terms: Public domain W3C validator