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

Theorem elrab2 3399
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 2722 . 2 (𝐴𝐶𝐴 ∈ {𝑥𝐵𝜑})
3 elrab2.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elrab 3396 . 2 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
52, 4bitri 264 1 (𝐴𝐶 ↔ (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233
This theorem is referenced by:  elrabsf  3507  pwnss  4860  fvmpti  6320  fvmptss2  6343  tfis  7096  elom  7110  oawordeulem  7679  oeeulem  7726  mapfienlem1  8351  mapfienlem3  8353  mapfien  8354  ordtypelem2  8465  ordtypelem3  8466  ordtypelem9  8472  wemapso2lem  8498  inf3lema  8559  oemapvali  8619  tz9.12lem3  8690  cofsmo  9129  enfin2i  9181  fin23lem28  9200  isf32lem6  9218  hsmexlem4  9289  zorn2lem2  9357  pwfseqlem1  9518  pwfseqlem3  9520  nqereu  9789  elz  11417  zsupss  11815  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  elrp  11872  repos  12308  wwlktovf  13745  wwlktovf1  13746  wwlktovfo  13747  sqrlem1  14027  sqrlem2  14028  sqrlem6  14032  sqrlem7  14033  ello1  14290  elo1  14301  rlimrege0  14354  divalglem2  15165  divalglem4  15166  divalglem5  15167  divalglem9  15171  divalglem10  15172  bitsfzolem  15203  gcdcllem1  15268  gcdcllem2  15269  gcdcllem3  15270  bezoutlem1  15303  bezoutlem3  15305  bezoutlem4  15306  isprm  15434  maxprmfct  15468  phimullem  15531  eulerthlem1  15533  eulerthlem2  15534  hashgcdlem  15540  pclem  15590  pcprecl  15591  pcprendvds  15592  infpn2  15664  prmreclem1  15667  prmreclem2  15668  prmreclem3  15669  prmreclem5  15671  1arith  15678  elgz  15682  4sqlem13  15708  4sqlem17  15712  4sqlem18  15713  vdwnnlem2  15747  vdwnnlem3  15748  ramtlecl  15751  isdrs  16981  istos  17082  islat  17094  isclat  17156  isdlat  17240  istsr  17264  issgrp  17332  ismnddef  17343  gsumvallem2  17419  isgrp  17475  elnmz  17680  gastacl  17788  gastacos  17789  symgfixelq  17899  psgneldm  17969  sylow1lem2  18060  sylow1lem4  18062  sylow2alem1  18078  sylow2alem2  18079  efgsdm  18189  iscmn  18246  iscyg  18327  iscyggen  18328  dprdw  18455  ablfacrplem  18510  ablfacrp  18511  ablfac1c  18516  ablfac1eu  18518  pgpfaclem1  18526  ablfaclem3  18532  ablfac2  18534  issrg  18553  isring  18597  iscrng  18600  isdrng  18799  islmod  18915  islvec  19152  lspsolvlem  19190  lbsextlem1  19206  lbsextlem3  19208  lbsextlem4  19209  islpir  19297  isnzr  19307  isrrg  19336  isdomn  19342  isassa  19363  psrbag  19412  psrbaglefi  19420  psrbagconcl  19421  psrbagconf1o  19422  gsumbagdiaglem  19423  mplelbas  19478  isphl  20021  pjdm  20099  ishil  20110  frlmssuvc1  20181  frlmssuvc2  20182  frlmsslsp  20183  gsummatr01lem1  20509  gsummatr01lem4  20512  gsummatr01  20513  mretopd  20944  neipeltop  20981  isperf  21003  ist0  21172  ist1  21173  ishaus  21174  iscnrm  21175  isreg  21184  isnrm  21187  ispnrm  21191  iscmp  21239  hauscmplem  21257  isconn  21264  conncompss  21284  is1stc  21292  islly  21319  isnlly  21320  dfac14lem  21468  ishmeo  21610  ptcmplem3  21905  ptcmplem4  21906  istmd  21925  istgp  21928  tgpconncompeqg  21962  tgpt0  21969  qustgpopn  21970  istrg  22014  istdrg  22016  istlm  22035  istvc  22042  iscusp  22150  imasdsf1olem  22225  isxms  22299  isms  22301  blcld  22357  prdsxmslem2  22381  isngp  22447  isnrg  22511  isnlm  22526  icccmplem1  22672  icccmplem2  22673  isclm  22910  iscph  23016  isbn  23181  iscms  23188  ivthlem1  23266  ivthlem2  23267  ivthlem3  23268  elovolm  23289  ovolicc2lem2  23332  ovolicc2lem4  23334  ovolicc2lem5  23335  ismbl  23340  dyadmbllem  23413  dyadmbl  23414  ismbf1  23438  isi1f  23486  isibl  23577  isuc1p  23945  ismon1p  23947  radcnvle  24219  abelthlem2  24231  abelthlem7a  24236  atans  24702  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem5  24804  lgambdd  24808  wilthlem2  24840  wilthlem3  24841  ftalem3  24846  sqff1o  24953  dvdsmulf1o  24965  lgslem2  25068  lgslem3  25069  lgsfcl2  25073  rpvmasumlem  25221  dchrvmaeq0  25238  dchrisum0re  25247  pntlem3  25343  axcontlem2  25890  lfgredgge2  26064  uspgredg2vlem  26160  uspgredg2v  26161  usgredg2vlem1  26162  usgredg2vlem2  26163  ushgredgedg  26166  ushgredgedgloop  26168  uhgrspan1  26240  upgrreslem  26241  umgrreslem  26242  isfusgr  26255  nbupgrres  26310  nbusgredgeu0  26314  uvtxel  26335  uvtxel1  26345  cusgrexilem2  26394  cusgrfilem2  26408  vtxdginducedm1lem4  26494  iswspthn  26798  wwlknon  26808  wspthnon  26809  wspthnonOLD  26811  wlknwwlksnfun  26842  wlknwwlksninj  26843  wlkwwlkfun  26849  wlkwwlkinj  26850  wlkwwlksur  26851  wwlksnextfun  26861  wwlksnextinj  26862  wwlksnextsur  26863  wwlksnextproplem3  26874  isclwwlkn  26987  clwwlkel  27009  clwwlkf  27010  clwwlkf1  27012  clwlksfclwwlk1hashn  27046  clwlksfoclwwlk  27050  clwlksf1clwwlklem0  27051  isclwwlknon  27065  frgrwopreglem3  27294  frgrwopreglem5lem  27300  frgrwopreglem5  27301  isablo  27528  iscbn  27848  hcau  28169  issh  28193  isch  28207  elcnop  28844  ellnop  28845  elbdop  28847  elhmop  28860  elcnfn  28869  ellnfn  28870  isst  29200  ishst  29201  ela  29326  isomnd  29829  isslmd  29883  isorng  29927  iscref  30039  isrrext  30172  ispisys  30343  isldsys  30347  isros  30359  issros  30366  oddpwdc  30544  eulerpartleme  30553  eulerpartlemo  30555  eulerpartlemd  30556  eulerpartlemt0  30559  eulerpartlemf  30560  eulerpartlemt  30561  eulerpartlemr  30564  eulerpartlemmf  30565  eulerpartlemgvv  30566  eulerpartlemgs2  30570  eulerpartlemn  30571  elprob  30599  ballotlemelo  30677  ballotleme  30686  bnj1152  31192  bnj1280  31214  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem1  31299  ispconn  31331  issconn  31334  cvmsiota  31385  cvmlift2lem12  31422  rdgprc0  31823  elwlim  31893  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  topdifinffinlem  33325  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  isprrngo  33979  rabeqel  34160  toycom  34578  isopos  34785  isoml  34843  isatl  34904  iscvlat  34928  ishlat1  34957  cdlemm10N  36724  dihglblem2N  36900  lcfl1lem  37097  lcfls1lem  37140  mapdordlem1a  37240  mapdordlem1  37242  pellqrex  37760  islnm  37964  pwssplit4  37976  islnr  37998  fnlimcnv  40217  stoweidlem14  40549  stoweidlem16  40551  stoweidlem37  40572  stoweidlem48  40583  stoweidlem51  40586  stoweidlem59  40594  salexct  40870  salexct2  40875  salexct3  40878  salgencntex  40879  salgensscntex  40880  ovn0lem  41100  opnvonmbllem1  41167  ovolval5lem2  41188  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  smfresal  41316  smfmullem2  41320  smfpimbor1lem1  41326  smfpimbor1lem2  41327  smfinflem  41344  iseven  41866  isodd  41867  m1expevenALTV  41885  iseven2  41889  isodd3  41890  odd2np1ALTV  41910  opoeALTV  41919  opeoALTV  41920  isgbe  41964  isgbow  41965  isgbo  41966  sprsymrelfo  42072  0nodd  42135  1odd  42136  2nodd  42137  iscmgmALT  42185  issgrpALT  42186  iscsgrpALT  42187  isrng  42201  1neven  42257  2zlidl  42259  2zrngamgm  42264  2zrngagrp  42268  2zrngmmgm  42271  2zrngnmrid  42275
  Copyright terms: Public domain W3C validator