Theorem elrab2 3662

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449

This theorem is referenced by:  rru  3750  elrabsf  3799  fvmpti  6967  fvmptss2  6994  tfis  7831  elom  7845  oawordeulem  8518  oeeulem  8565  mapfienlem1  9356  mapfienlem3  9358  mapfien  9359  ordtypelem2  9472  ordtypelem3  9473  ordtypelem9  9479  wemapso2lem  9505  inf3lema  9577  oemapvali  9637  tz9.12lem3  9742  cofsmo  10222  enfin2i  10274  fin23lem28  10293  isf32lem6  10311  hsmexlem4  10382  zorn2lem2  10450  pwfseqlem1  10611  pwfseqlem3  10613  nqereu  10882  elz  12531  zsupss  12896  rpnnen1lem5  12940  elrp  12953  repos  13407  wwlktovf  14922  wwlktovf1  14923  wwlktovfo  14924  01sqrexlem1  15208  01sqrexlem2  15209  01sqrexlem6  15213  01sqrexlem7  15214  ello1  15481  elo1  15492  rlimrege0  15545  divalglem2  16365  divalglem4  16366  divalglem5  16367  divalglem9  16371  divalglem10  16372  bitsfzolem  16404  gcdcllem1  16469  gcdcllem2  16470  gcdcllem3  16471  bezoutlem1  16509  bezoutlem3  16511  bezoutlem4  16512  isprm  16643  maxprmfct  16679  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  hashgcdlem  16758  pclem  16809  pcprecl  16810  pcprendvds  16811  infpn2  16884  prmreclem1  16887  prmreclem2  16888  prmreclem3  16889  prmreclem5  16891  1arith  16898  elgz  16902  4sqlem13  16928  4sqlem17  16932  4sqlem18  16933  vdwnnlem2  16967  vdwnnlem3  16968  ramtlecl  16971  isdrs  18262  istos  18377  islat  18392  isclat  18459  isdlat  18481  istsr  18542  issgrp  18647  ismnddef  18663  gsumvallem2  18761  isgrp  18871  elnmz  19095  gastacl  19241  gastacos  19242  symgfixelq  19363  psgneldm  19433  sylow1lem2  19529  sylow1lem4  19531  sylow2alem1  19547  sylow2alem2  19548  efgsdm  19660  iscmn  19719  iscyg  19809  iscyggen  19810  dprdw  19942  ablfacrplem  19997  ablfacrp  19998  ablfac1c  20003  ablfac1eu  20005  pgpfaclem1  20013  ablfaclem3  20019  ablfac2  20021  issimpg  20024  isrng  20063  issrg  20097  isring  20146  iscrng  20149  isnzr  20423  islring  20449  isrrg  20607  isdomn  20614  isdrng  20642  islmod  20770  islvec  21011  lspsolvlem  21052  lbsextlem1  21068  lbsextlem3  21070  lbsextlem4  21071  islpir  21238  isphl  21537  pjdm  21616  ishil  21627  frlmssuvc1  21703  frlmssuvc2  21704  frlmsslsp  21705  isassa  21765  psrbag  21826  psrbaglefi  21835  psrbagconcl  21836  psrbagleadd1  21837  gsumbagdiaglem  21839  mplelbas  21900  gsummatr01lem1  22542  gsummatr01lem4  22545  gsummatr01  22546  mretopd  22979  neipeltop  23016  isperf  23038  ist0  23207  ist1  23208  ishaus  23209  iscnrm  23210  isreg  23219  isnrm  23222  ispnrm  23226  iscmp  23275  hauscmplem  23293  isconn  23300  conncompss  23320  is1stc  23328  islly  23355  isnlly  23356  dfac14lem  23504  ishmeo  23646  ptcmplem3  23941  ptcmplem4  23942  istmd  23961  istgp  23964  tgpconncompeqg  23999  tgpt0  24006  qustgpopn  24007  istrg  24051  istdrg  24053  istlm  24072  istvc  24079  iscusp  24186  imasdsf1olem  24261  isxms  24335  isms  24337  blcld  24393  prdsxmslem2  24417  isngp  24484  isnrg  24548  isnlm  24563  icccmplem1  24711  icccmplem2  24712  isclm  24964  iscph  25070  isbn  25238  iscms  25245  ivthlem1  25352  ivthlem2  25353  ivthlem3  25354  elovolm  25376  ovolicc2lem2  25419  ovolicc2lem4  25421  ovolicc2lem5  25422  ismbl  25427  dyadmbllem  25500  dyadmbl  25501  ismbf1  25525  isi1f  25575  isibl  25666  isuc1p  26046  ismon1p  26048  radcnvle  26329  abelthlem2  26342  abelthlem7a  26347  atans  26840  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  lgambdd  26947  wilthlem2  26979  wilthlem3  26980  ftalem3  26985  sqff1o  27092  mpodvdsmulf1o  27104  dvdsmulf1o  27106  lgslem2  27209  lgslem3  27210  lgsfcl2  27214  rpvmasumlem  27398  dchrvmaeq0  27415  dchrisum0re  27424  pntlem3  27520  elleft  27773  elright  27774  elons  28154  elreno  28346  axcontlem2  28892  lfgredgge2  29051  uspgredg2vlem  29150  uspgredg2v  29151  usgredg2vlem1  29152  usgredg2vlem2  29153  ushgredgedg  29156  ushgredgedgloop  29158  uhgrspan1  29230  upgrreslem  29231  umgrreslem  29232  isfusgr  29245  nbupgrres  29291  nbusgredgeu0  29295  nbusgrf1o0  29296  uvtxel  29315  uvtxel1  29323  cusgrexilem2  29369  cusgrfilem2  29384  vtxdginducedm1lem4  29470  rgrx0ndm  29521  iswspthn  29779  wwlknon  29787  wspthnon  29788  wwlksn0  29793  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextsurj  29830  wwlksnextproplem3  29841  clwlkclwwlkflem  29933  clwlkclwwlkfolem  29936  isclwwlkn  29956  clwwlkel  29975  clwwlkf  29976  clwwlkf1  29978  isclwwlknon  30020  s2elclwwlknon2  30033  isfrgr  30189  frgrwopreglem3  30243  frgrwopreglem5lem  30249  frgrwopreglem5  30250  isablo  30475  iscbn  30793  hcau  31113  issh  31137  isch  31151  elcnop  31786  ellnop  31787  elbdop  31789  elhmop  31802  elcnfn  31811  ellnfn  31812  isst  32142  ishst  32143  ela  32268  ischn  32932  isomnd  33015  isslmd  33155  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspn  33197  isorng  33277  ssdifidllem  33427  ssdifidlprm  33429  ssmxidllem  33444  isufd  33511  iscref  33834  isrrext  33990  ispisys  34142  isldsys  34146  isros  34158  issros  34165  oddpwdc  34345  eulerpartleme  34354  eulerpartlemo  34356  eulerpartlemd  34357  eulerpartlemt0  34360  eulerpartlemf  34361  eulerpartlemt  34362  eulerpartlemr  34365  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgs2  34371  eulerpartlemn  34372  elprob  34400  ballotlemelo  34479  ballotleme  34488  bnj1152  34988  bnj1280  35010  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem1  35178  ispconn  35210  issconn  35213  cvmsiota  35264  cvmlift2lem12  35301  fmla1  35374  gonan0  35379  goaln0  35380  gonar  35382  goalr  35384  sategoelfvb  35406  rdgprc0  35781  elwlim  35811  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  topdifinffinlem  37335  pibp19  37402  pibp21  37403  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  isprrngo  38044  rabeqel  38243  toycom  38966  isopos  39173  isoml  39231  isatl  39292  iscvlat  39316  ishlat1  39345  cdlemm10N  41112  dihglblem2N  41288  lcfl1lem  41485  lcfls1lem  41528  mapdordlem1a  41628  mapdordlem1  41630  iscsrg  41958  readvcot  42352  mhphflem  42584  pellqrex  42867  islnm  43066  pwssplit4  43078  islnr  43100  fnlimcnv  45665  stoweidlem14  46012  stoweidlem16  46014  stoweidlem37  46035  stoweidlem48  46046  stoweidlem51  46049  stoweidlem59  46057  salexct  46332  salexct2  46337  salexct3  46340  salgencntex  46341  salgensscntex  46342  ovn0lem  46563  opnvonmbllem1  46630  ovolval5lem2  46651  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  smfresal  46786  smfmullem2  46790  smfpimbor1lem1  46796  smfpimbor1lem2  46797  smfinflem  46815  sprsymrelfo  47498  prproropf1olem1  47504  pairreueq  47511  iseven  47629  isodd  47630  m1expevenALTV  47648  iseven2  47652  isodd3  47653  odd2np1ALTV  47675  opoeALTV  47684  opeoALTV  47685  isgbe  47752  isgbow  47753  isgbo  47754  uspgrlimlem2  47988  uspgrlimlem3  47989  uspgrlimlem4  47990  0nodd  48158  1odd  48159  2nodd  48160  iscmgmALT  48212  issgrpALT  48213  iscsgrpALT  48214  1neven  48226  2zlidl  48228  2zrngamgm  48233  2zrngagrp  48237  2zrngmmgm  48240  2zrngnmrid  48244  itsclc0  48760  itsclc0b  48761  isthinc  49408  istermc  49463