Theorem elrab2 3628

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 2831	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 3625	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 274	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2107  {crab 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435

This theorem is referenced by:  rru  3715  elrabsf  3765  fvmpti  6883  fvmptss2  6909  tfis  7710  elom  7724  oawordeulem  8394  oeeulem  8441  mapfienlem1  9173  mapfienlem3  9175  mapfien  9176  ordtypelem2  9287  ordtypelem3  9288  ordtypelem9  9294  wemapso2lem  9320  inf3lema  9391  oemapvali  9451  tz9.12lem3  9556  cofsmo  10034  enfin2i  10086  fin23lem28  10105  isf32lem6  10123  hsmexlem4  10194  zorn2lem2  10262  pwfseqlem1  10423  pwfseqlem3  10425  nqereu  10694  elz  12330  zsupss  12686  rpnnen1lem5  12730  elrp  12741  repos  13187  wwlktovf  14680  wwlktovf1  14681  wwlktovfo  14682  sqrlem1  14963  sqrlem2  14964  sqrlem6  14968  sqrlem7  14969  ello1  15233  elo1  15244  rlimrege0  15297  divalglem2  16113  divalglem4  16114  divalglem5  16115  divalglem9  16119  divalglem10  16120  bitsfzolem  16150  gcdcllem1  16215  gcdcllem2  16216  gcdcllem3  16217  bezoutlem1  16256  bezoutlem3  16258  bezoutlem4  16259  isprm  16387  maxprmfct  16423  phimullem  16489  eulerthlem1  16491  eulerthlem2  16492  hashgcdlem  16498  pclem  16548  pcprecl  16549  pcprendvds  16550  infpn2  16623  prmreclem1  16626  prmreclem2  16627  prmreclem3  16628  prmreclem5  16630  1arith  16637  elgz  16641  4sqlem13  16667  4sqlem17  16671  4sqlem18  16672  vdwnnlem2  16706  vdwnnlem3  16707  ramtlecl  16710  isdrs  18028  istos  18145  islat  18160  isclat  18227  isdlat  18249  istsr  18310  issgrp  18385  ismnddef  18396  gsumvallem2  18481  isgrp  18592  elnmz  18800  gastacl  18924  gastacos  18925  symgfixelq  19050  psgneldm  19120  sylow1lem2  19213  sylow1lem4  19215  sylow2alem1  19231  sylow2alem2  19232  efgsdm  19345  iscmn  19403  iscyg  19488  iscyggen  19489  dprdw  19622  ablfacrplem  19677  ablfacrp  19678  ablfac1c  19683  ablfac1eu  19685  pgpfaclem1  19693  ablfaclem3  19699  ablfac2  19701  issimpg  19704  issrg  19752  isring  19796  iscrng  19799  isdrng  20004  islmod  20136  islvec  20375  lspsolvlem  20413  lbsextlem1  20429  lbsextlem3  20431  lbsextlem4  20432  islpir  20529  isnzr  20539  isrrg  20568  isdomn  20574  isphl  20842  pjdm  20923  ishil  20934  frlmssuvc1  21010  frlmssuvc2  21011  frlmsslsp  21012  isassa  21072  psrbag  21129  psrbaglefi  21144  psrbaglefiOLD  21145  psrbagconcl  21146  psrbagconclOLD  21147  psrbagconf1oOLD  21149  gsumbagdiaglemOLD  21150  gsumbagdiaglem  21153  mplelbas  21208  gsummatr01lem1  21813  gsummatr01lem4  21816  gsummatr01  21817  mretopd  22252  neipeltop  22289  isperf  22311  ist0  22480  ist1  22481  ishaus  22482  iscnrm  22483  isreg  22492  isnrm  22495  ispnrm  22499  iscmp  22548  hauscmplem  22566  isconn  22573  conncompss  22593  is1stc  22601  islly  22628  isnlly  22629  dfac14lem  22777  ishmeo  22919  ptcmplem3  23214  ptcmplem4  23215  istmd  23234  istgp  23237  tgpconncompeqg  23272  tgpt0  23279  qustgpopn  23280  istrg  23324  istdrg  23326  istlm  23345  istvc  23352  iscusp  23460  imasdsf1olem  23535  isxms  23609  isms  23611  blcld  23670  prdsxmslem2  23694  isngp  23761  isnrg  23833  isnlm  23848  icccmplem1  23994  icccmplem2  23995  isclm  24236  iscph  24343  isbn  24511  iscms  24518  ivthlem1  24624  ivthlem2  24625  ivthlem3  24626  elovolm  24648  ovolicc2lem2  24691  ovolicc2lem4  24693  ovolicc2lem5  24694  ismbl  24699  dyadmbllem  24772  dyadmbl  24773  ismbf1  24797  isi1f  24847  isibl  24939  isuc1p  25314  ismon1p  25316  radcnvle  25588  abelthlem2  25600  abelthlem7a  25605  atans  26089  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgambdd  26195  wilthlem2  26227  wilthlem3  26228  ftalem3  26233  sqff1o  26340  dvdsmulf1o  26352  lgslem2  26455  lgslem3  26456  lgsfcl2  26460  rpvmasumlem  26644  dchrvmaeq0  26661  dchrisum0re  26670  pntlem3  26766  axcontlem2  27342  lfgredgge2  27503  uspgredg2vlem  27599  uspgredg2v  27600  usgredg2vlem1  27601  usgredg2vlem2  27602  ushgredgedg  27605  ushgredgedgloop  27607  uhgrspan1  27679  upgrreslem  27680  umgrreslem  27681  isfusgr  27694  nbupgrres  27740  nbusgredgeu0  27744  nbusgrf1o0  27745  uvtxel  27764  uvtxel1  27772  cusgrexilem2  27818  cusgrfilem2  27832  vtxdginducedm1lem4  27918  rgrx0ndm  27969  iswspthn  28223  wwlknon  28231  wspthnon  28232  wwlksn0  28237  wwlksnextfun  28272  wwlksnextinj  28273  wwlksnextsurj  28274  wwlksnextproplem3  28285  clwlkclwwlkflem  28377  clwlkclwwlkfolem  28380  isclwwlkn  28400  clwwlkel  28419  clwwlkf  28420  clwwlkf1  28422  isclwwlknon  28464  s2elclwwlknon2  28477  isfrgr  28633  frgrwopreglem3  28687  frgrwopreglem5lem  28693  frgrwopreglem5  28694  isablo  28917  iscbn  29235  hcau  29555  issh  29579  isch  29593  elcnop  30228  ellnop  30229  elbdop  30231  elhmop  30244  elcnfn  30253  ellnfn  30254  isst  30584  ishst  30585  ela  30710  isomnd  31336  isslmd  31464  isorng  31507  ssmxidllem  31650  isufd  31672  iscref  31803  isrrext  31959  ispisys  32129  isldsys  32133  isros  32145  issros  32152  oddpwdc  32330  eulerpartleme  32339  eulerpartlemo  32341  eulerpartlemd  32342  eulerpartlemt0  32345  eulerpartlemf  32346  eulerpartlemt  32347  eulerpartlemr  32350  eulerpartlemmf  32351  eulerpartlemgvv  32352  eulerpartlemgs2  32356  eulerpartlemn  32357  elprob  32385  ballotlemelo  32463  ballotleme  32472  bnj1152  32987  bnj1280  33009  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem1  33162  ispconn  33194  issconn  33197  cvmsiota  33248  cvmlift2lem12  33285  fmla1  33358  gonan0  33363  goaln0  33364  gonar  33366  goalr  33368  sategoelfvb  33390  rdgprc0  33778  elwlim  33826  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  topdifinffinlem  35527  pibp19  35594  pibp21  35595  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  isprrngo  36217  rabeqel  36402  toycom  36994  isopos  37201  isoml  37259  isatl  37320  iscvlat  37344  ishlat1  37373  cdlemm10N  39139  dihglblem2N  39315  lcfl1lem  39512  lcfls1lem  39555  mapdordlem1a  39655  mapdordlem1  39657  mhphflem  40291  pellqrex  40708  islnm  40909  pwssplit4  40921  islnr  40943  fnlimcnv  43215  stoweidlem14  43562  stoweidlem16  43564  stoweidlem37  43585  stoweidlem48  43596  stoweidlem51  43599  stoweidlem59  43607  salexct  43880  salexct2  43885  salexct3  43888  salgencntex  43889  salgensscntex  43890  ovn0lem  44110  opnvonmbllem1  44177  ovolval5lem2  44198  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  smfresal  44333  smfmullem2  44337  smfpimbor1lem1  44343  smfpimbor1lem2  44344  smfinflem  44361  sprsymrelfo  44960  prproropf1olem1  44966  pairreueq  44973  iseven  45091  isodd  45092  m1expevenALTV  45110  iseven2  45114  isodd3  45115  odd2np1ALTV  45137  opoeALTV  45146  opeoALTV  45147  isgbe  45214  isgbow  45215  isgbo  45216  0nodd  45375  1odd  45376  2nodd  45377  iscmgmALT  45429  issgrpALT  45430  iscsgrpALT  45431  isrng  45445  1neven  45501  2zlidl  45503  2zrngamgm  45508  2zrngagrp  45512  2zrngmmgm  45515  2zrngnmrid  45519  itsclc0  46128  itsclc0b  46129  isthinc  46313