Theorem elrab2 3651

Description: Membership in a restricted 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

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2829	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 3648	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 275	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444

This theorem is referenced by:  rru  3739  elrabsf  3788  fvmpti  6948  fvmptss2  6976  tfis  7807  elom  7821  oawordeulem  8491  oeeulem  8539  mapfienlem1  9320  mapfienlem3  9322  mapfien  9323  ordtypelem2  9436  ordtypelem3  9437  ordtypelem9  9443  wemapso2lem  9469  inf3lema  9545  oemapvali  9605  tz9.12lem3  9713  cofsmo  10191  enfin2i  10243  fin23lem28  10262  isf32lem6  10280  hsmexlem4  10351  zorn2lem2  10419  pwfseqlem1  10581  pwfseqlem3  10583  nqereu  10852  elz  12502  zsupss  12862  rpnnen1lem5  12906  elrp  12919  repos  13374  wwlktovf  14891  wwlktovf1  14892  wwlktovfo  14893  01sqrexlem1  15177  01sqrexlem2  15178  01sqrexlem6  15182  01sqrexlem7  15183  ello1  15450  elo1  15461  rlimrege0  15514  divalglem2  16334  divalglem4  16335  divalglem5  16336  divalglem9  16340  divalglem10  16341  bitsfzolem  16373  gcdcllem1  16438  gcdcllem2  16439  gcdcllem3  16440  bezoutlem1  16478  bezoutlem3  16480  bezoutlem4  16481  isprm  16612  maxprmfct  16648  phimullem  16718  eulerthlem1  16720  eulerthlem2  16721  hashgcdlem  16727  pclem  16778  pcprecl  16779  pcprendvds  16780  infpn2  16853  prmreclem1  16856  prmreclem2  16857  prmreclem3  16858  prmreclem5  16860  1arith  16867  elgz  16871  4sqlem13  16897  4sqlem17  16901  4sqlem18  16902  vdwnnlem2  16936  vdwnnlem3  16937  ramtlecl  16940  isdrs  18236  istos  18351  islat  18368  isclat  18435  isdlat  18457  istsr  18518  ischn  18542  issgrp  18657  ismnddef  18673  gsumvallem2  18771  isgrp  18881  elnmz  19104  gastacl  19250  gastacos  19251  symgfixelq  19374  psgneldm  19444  sylow1lem2  19540  sylow1lem4  19542  sylow2alem1  19558  sylow2alem2  19559  efgsdm  19671  iscmn  19730  iscyg  19820  iscyggen  19821  dprdw  19953  ablfacrplem  20008  ablfacrp  20009  ablfac1c  20014  ablfac1eu  20016  pgpfaclem1  20024  ablfaclem3  20030  ablfac2  20032  issimpg  20035  isomnd  20064  isrng  20101  issrg  20135  isring  20184  iscrng  20187  isnzr  20459  islring  20485  isrrg  20643  isdomn  20650  isdrng  20678  isorng  20806  islmod  20827  islvec  21068  lspsolvlem  21109  lbsextlem1  21125  lbsextlem3  21127  lbsextlem4  21128  islpir  21295  isphl  21595  pjdm  21674  ishil  21685  frlmssuvc1  21761  frlmssuvc2  21762  frlmsslsp  21763  isassa  21823  psrbag  21885  psrbaglefi  21894  psrbagconcl  21895  psrbagleadd1  21896  gsumbagdiaglem  21898  mplelbas  21958  gsummatr01lem1  22611  gsummatr01lem4  22614  gsummatr01  22615  mretopd  23048  neipeltop  23085  isperf  23107  ist0  23276  ist1  23277  ishaus  23278  iscnrm  23279  isreg  23288  isnrm  23291  ispnrm  23295  iscmp  23344  hauscmplem  23362  isconn  23369  conncompss  23389  is1stc  23397  islly  23424  isnlly  23425  dfac14lem  23573  ishmeo  23715  ptcmplem3  24010  ptcmplem4  24011  istmd  24030  istgp  24033  tgpconncompeqg  24068  tgpt0  24075  qustgpopn  24076  istrg  24120  istdrg  24122  istlm  24141  istvc  24148  iscusp  24254  imasdsf1olem  24329  isxms  24403  isms  24405  blcld  24461  prdsxmslem2  24485  isngp  24552  isnrg  24616  isnlm  24631  icccmplem1  24779  icccmplem2  24780  isclm  25032  iscph  25138  isbn  25306  iscms  25313  ivthlem1  25420  ivthlem2  25421  ivthlem3  25422  elovolm  25444  ovolicc2lem2  25487  ovolicc2lem4  25489  ovolicc2lem5  25490  ismbl  25495  dyadmbllem  25568  dyadmbl  25569  ismbf1  25593  isi1f  25643  isibl  25734  isuc1p  26114  ismon1p  26116  radcnvle  26397  abelthlem2  26410  abelthlem7a  26415  atans  26908  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem5  27011  lgambdd  27015  wilthlem2  27047  wilthlem3  27048  ftalem3  27053  sqff1o  27160  mpodvdsmulf1o  27172  dvdsmulf1o  27174  lgslem2  27277  lgslem3  27278  lgsfcl2  27282  rpvmasumlem  27466  dchrvmaeq0  27483  dchrisum0re  27492  pntlem3  27588  elleft  27859  elright  27860  elons  28261  elreno  28499  axcontlem2  29050  lfgredgge2  29209  uspgredg2vlem  29308  uspgredg2v  29309  usgredg2vlem1  29310  usgredg2vlem2  29311  ushgredgedg  29314  ushgredgedgloop  29316  uhgrspan1  29388  upgrreslem  29389  umgrreslem  29390  isfusgr  29403  nbupgrres  29449  nbusgredgeu0  29453  nbusgrf1o0  29454  uvtxel  29473  uvtxel1  29481  cusgrexilem2  29527  cusgrfilem2  29542  vtxdginducedm1lem4  29628  rgrx0ndm  29679  iswspthn  29934  wwlknon  29942  wspthnon  29943  wwlksn0  29948  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextsurj  29985  wwlksnextproplem3  29996  clwlkclwwlkflem  30091  clwlkclwwlkfolem  30094  isclwwlkn  30114  clwwlkel  30133  clwwlkf  30134  clwwlkf1  30136  isclwwlknon  30178  s2elclwwlknon2  30191  isfrgr  30347  frgrwopreglem3  30401  frgrwopreglem5lem  30407  frgrwopreglem5  30408  isablo  30634  iscbn  30952  hcau  31272  issh  31296  isch  31310  elcnop  31945  ellnop  31946  elbdop  31948  elhmop  31961  elcnfn  31970  ellnfn  31971  isst  32301  ishst  32302  ela  32427  isslmd  33296  elrgspnlem1  33336  elrgspnlem2  33337  elrgspnlem4  33339  elrgspn  33340  ssdifidllem  33549  ssdifidlprm  33551  ssmxidllem  33566  isufd  33633  iscref  34022  isrrext  34178  ispisys  34330  isldsys  34334  isros  34346  issros  34353  oddpwdc  34532  eulerpartleme  34541  eulerpartlemo  34543  eulerpartlemd  34544  eulerpartlemt0  34547  eulerpartlemf  34548  eulerpartlemt  34549  eulerpartlemr  34552  eulerpartlemmf  34553  eulerpartlemgvv  34554  eulerpartlemgs2  34558  eulerpartlemn  34559  elprob  34587  ballotlemelo  34666  ballotleme  34675  bnj1152  35174  bnj1280  35196  subfacp1lem3  35398  subfacp1lem5  35400  erdszelem1  35407  ispconn  35439  issconn  35442  cvmsiota  35493  cvmlift2lem12  35530  fmla1  35603  gonan0  35608  goaln0  35609  gonar  35611  goalr  35613  sategoelfvb  35635  rdgprc0  36007  elwlim  36037  neibastop1  36575  neibastop2lem  36576  neibastop2  36577  topdifinffinlem  37602  pibp19  37669  pibp21  37670  poimirlem5  37876  poimirlem6  37877  poimirlem7  37878  poimirlem8  37879  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem15  37886  poimirlem16  37887  poimirlem17  37888  poimirlem18  37889  poimirlem19  37890  poimirlem20  37891  poimirlem21  37892  poimirlem22  37893  isprrngo  38301  rabeqel  38508  toycom  39349  isopos  39556  isoml  39614  isatl  39675  iscvlat  39699  ishlat1  39728  cdlemm10N  41494  dihglblem2N  41670  lcfl1lem  41867  lcfls1lem  41910  mapdordlem1a  42010  mapdordlem1  42012  iscsrg  42340  readvcot  42734  mhphflem  42954  pellqrex  43236  islnm  43434  pwssplit4  43446  islnr  43468  fnlimcnv  46025  stoweidlem14  46372  stoweidlem16  46374  stoweidlem37  46395  stoweidlem48  46406  stoweidlem51  46409  stoweidlem59  46417  salexct  46692  salexct2  46697  salexct3  46700  salgencntex  46701  salgensscntex  46702  ovn0lem  46923  opnvonmbllem1  46990  ovolval5lem2  47011  pimincfltioc  47074  pimdecfgtioo  47075  pimincfltioo  47076  smfresal  47146  smfmullem2  47150  smfpimbor1lem1  47156  smfpimbor1lem2  47157  smfinflem  47175  sprsymrelfo  47857  prproropf1olem1  47863  pairreueq  47870  iseven  47988  isodd  47989  m1expevenALTV  48007  iseven2  48011  isodd3  48012  odd2np1ALTV  48034  opoeALTV  48043  opeoALTV  48044  isgbe  48111  isgbow  48112  isgbo  48113  uspgrlimlem2  48349  uspgrlimlem3  48350  uspgrlimlem4  48351  clnbgrvtxedg  48354  grlimpredg  48358  grlimprclnbgrvtx  48359  grlimgrtrilem1  48361  0nodd  48530  1odd  48531  2nodd  48532  iscmgmALT  48584  issgrpALT  48585  iscsgrpALT  48586  1neven  48598  2zlidl  48600  2zrngamgm  48605  2zrngagrp  48609  2zrngmmgm  48612  2zrngnmrid  48616  itsclc0  49131  itsclc0b  49132  isthinc  49778  istermc  49833