Theorem elrab2 3695

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482

This theorem is referenced by:  rru  3785  elrabsf  3834  fvmpti  7015  fvmptss2  7042  tfis  7876  elom  7890  oawordeulem  8592  oeeulem  8639  mapfienlem1  9445  mapfienlem3  9447  mapfien  9448  ordtypelem2  9559  ordtypelem3  9560  ordtypelem9  9566  wemapso2lem  9592  inf3lema  9664  oemapvali  9724  tz9.12lem3  9829  cofsmo  10309  enfin2i  10361  fin23lem28  10380  isf32lem6  10398  hsmexlem4  10469  zorn2lem2  10537  pwfseqlem1  10698  pwfseqlem3  10700  nqereu  10969  elz  12615  zsupss  12979  rpnnen1lem5  13023  elrp  13036  repos  13486  wwlktovf  14995  wwlktovf1  14996  wwlktovfo  14997  01sqrexlem1  15281  01sqrexlem2  15282  01sqrexlem6  15286  01sqrexlem7  15287  ello1  15551  elo1  15562  rlimrege0  15615  divalglem2  16432  divalglem4  16433  divalglem5  16434  divalglem9  16438  divalglem10  16439  bitsfzolem  16471  gcdcllem1  16536  gcdcllem2  16537  gcdcllem3  16538  bezoutlem1  16576  bezoutlem3  16578  bezoutlem4  16579  isprm  16710  maxprmfct  16746  phimullem  16816  eulerthlem1  16818  eulerthlem2  16819  hashgcdlem  16825  pclem  16876  pcprecl  16877  pcprendvds  16878  infpn2  16951  prmreclem1  16954  prmreclem2  16955  prmreclem3  16956  prmreclem5  16958  1arith  16965  elgz  16969  4sqlem13  16995  4sqlem17  16999  4sqlem18  17000  vdwnnlem2  17034  vdwnnlem3  17035  ramtlecl  17038  isdrs  18347  istos  18463  islat  18478  isclat  18545  isdlat  18567  istsr  18628  issgrp  18733  ismnddef  18749  gsumvallem2  18847  isgrp  18957  elnmz  19181  gastacl  19327  gastacos  19328  symgfixelq  19451  psgneldm  19521  sylow1lem2  19617  sylow1lem4  19619  sylow2alem1  19635  sylow2alem2  19636  efgsdm  19748  iscmn  19807  iscyg  19897  iscyggen  19898  dprdw  20030  ablfacrplem  20085  ablfacrp  20086  ablfac1c  20091  ablfac1eu  20093  pgpfaclem1  20101  ablfaclem3  20107  ablfac2  20109  issimpg  20112  isrng  20151  issrg  20185  isring  20234  iscrng  20237  isnzr  20514  islring  20540  isrrg  20698  isdomn  20705  isdrng  20733  islmod  20862  islvec  21103  lspsolvlem  21144  lbsextlem1  21160  lbsextlem3  21162  lbsextlem4  21163  islpir  21338  isphl  21646  pjdm  21727  ishil  21738  frlmssuvc1  21814  frlmssuvc2  21815  frlmsslsp  21816  isassa  21876  psrbag  21937  psrbaglefi  21946  psrbagconcl  21947  psrbagleadd1  21948  gsumbagdiaglem  21950  mplelbas  22011  gsummatr01lem1  22661  gsummatr01lem4  22664  gsummatr01  22665  mretopd  23100  neipeltop  23137  isperf  23159  ist0  23328  ist1  23329  ishaus  23330  iscnrm  23331  isreg  23340  isnrm  23343  ispnrm  23347  iscmp  23396  hauscmplem  23414  isconn  23421  conncompss  23441  is1stc  23449  islly  23476  isnlly  23477  dfac14lem  23625  ishmeo  23767  ptcmplem3  24062  ptcmplem4  24063  istmd  24082  istgp  24085  tgpconncompeqg  24120  tgpt0  24127  qustgpopn  24128  istrg  24172  istdrg  24174  istlm  24193  istvc  24200  iscusp  24308  imasdsf1olem  24383  isxms  24457  isms  24459  blcld  24518  prdsxmslem2  24542  isngp  24609  isnrg  24681  isnlm  24696  icccmplem1  24844  icccmplem2  24845  isclm  25097  iscph  25204  isbn  25372  iscms  25379  ivthlem1  25486  ivthlem2  25487  ivthlem3  25488  elovolm  25510  ovolicc2lem2  25553  ovolicc2lem4  25555  ovolicc2lem5  25556  ismbl  25561  dyadmbllem  25634  dyadmbl  25635  ismbf1  25659  isi1f  25709  isibl  25800  isuc1p  26180  ismon1p  26182  radcnvle  26463  abelthlem2  26476  abelthlem7a  26481  atans  26973  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem5  27076  lgambdd  27080  wilthlem2  27112  wilthlem3  27113  ftalem3  27118  sqff1o  27225  mpodvdsmulf1o  27237  dvdsmulf1o  27239  lgslem2  27342  lgslem3  27343  lgsfcl2  27347  rpvmasumlem  27531  dchrvmaeq0  27548  dchrisum0re  27557  pntlem3  27653  0elleft  27948  0elright  27949  addsproplem4  28005  addsproplem5  28006  addsproplem6  28007  negsproplem4  28063  negsproplem5  28064  mulsproplem12  28153  precsexlem8  28238  precsexlem9  28239  precsexlem11  28241  elons  28276  sltonold  28283  elreno  28427  axcontlem2  28980  lfgredgge2  29141  uspgredg2vlem  29240  uspgredg2v  29241  usgredg2vlem1  29242  usgredg2vlem2  29243  ushgredgedg  29246  ushgredgedgloop  29248  uhgrspan1  29320  upgrreslem  29321  umgrreslem  29322  isfusgr  29335  nbupgrres  29381  nbusgredgeu0  29385  nbusgrf1o0  29386  uvtxel  29405  uvtxel1  29413  cusgrexilem2  29459  cusgrfilem2  29474  vtxdginducedm1lem4  29560  rgrx0ndm  29611  iswspthn  29869  wwlknon  29877  wspthnon  29878  wwlksn0  29883  wwlksnextfun  29918  wwlksnextinj  29919  wwlksnextsurj  29920  wwlksnextproplem3  29931  clwlkclwwlkflem  30023  clwlkclwwlkfolem  30026  isclwwlkn  30046  clwwlkel  30065  clwwlkf  30066  clwwlkf1  30068  isclwwlknon  30110  s2elclwwlknon2  30123  isfrgr  30279  frgrwopreglem3  30333  frgrwopreglem5lem  30339  frgrwopreglem5  30340  isablo  30565  iscbn  30883  hcau  31203  issh  31227  isch  31241  elcnop  31876  ellnop  31877  elbdop  31879  elhmop  31892  elcnfn  31901  ellnfn  31902  isst  32232  ishst  32233  ela  32358  ischn  32996  isomnd  33078  isslmd  33208  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspn  33250  isorng  33329  ssdifidllem  33484  ssdifidlprm  33486  ssmxidllem  33501  isufd  33568  iscref  33843  isrrext  34001  ispisys  34153  isldsys  34157  isros  34169  issros  34176  oddpwdc  34356  eulerpartleme  34365  eulerpartlemo  34367  eulerpartlemd  34368  eulerpartlemt0  34371  eulerpartlemf  34372  eulerpartlemt  34373  eulerpartlemr  34376  eulerpartlemmf  34377  eulerpartlemgvv  34378  eulerpartlemgs2  34382  eulerpartlemn  34383  elprob  34411  ballotlemelo  34490  ballotleme  34499  bnj1152  35012  bnj1280  35034  subfacp1lem3  35187  subfacp1lem5  35189  erdszelem1  35196  ispconn  35228  issconn  35231  cvmsiota  35282  cvmlift2lem12  35319  fmla1  35392  gonan0  35397  goaln0  35398  gonar  35400  goalr  35402  sategoelfvb  35424  rdgprc0  35794  elwlim  35824  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  topdifinffinlem  37348  pibp19  37415  pibp21  37416  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  isprrngo  38057  rabeqel  38255  toycom  38974  isopos  39181  isoml  39239  isatl  39300  iscvlat  39324  ishlat1  39353  cdlemm10N  41120  dihglblem2N  41296  lcfl1lem  41493  lcfls1lem  41536  mapdordlem1a  41636  mapdordlem1  41638  iscsrg  41970  readvcot  42394  mhphflem  42606  pellqrex  42890  islnm  43089  pwssplit4  43101  islnr  43123  fnlimcnv  45682  stoweidlem14  46029  stoweidlem16  46031  stoweidlem37  46052  stoweidlem48  46063  stoweidlem51  46066  stoweidlem59  46074  salexct  46349  salexct2  46354  salexct3  46357  salgencntex  46358  salgensscntex  46359  ovn0lem  46580  opnvonmbllem1  46647  ovolval5lem2  46668  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  smfresal  46803  smfmullem2  46807  smfpimbor1lem1  46813  smfpimbor1lem2  46814  smfinflem  46832  sprsymrelfo  47484  prproropf1olem1  47490  pairreueq  47497  iseven  47615  isodd  47616  m1expevenALTV  47634  iseven2  47638  isodd3  47639  odd2np1ALTV  47661  opoeALTV  47670  opeoALTV  47671  isgbe  47738  isgbow  47739  isgbo  47740  uspgrlimlem2  47956  uspgrlimlem3  47957  uspgrlimlem4  47958  0nodd  48086  1odd  48087  2nodd  48088  iscmgmALT  48140  issgrpALT  48141  iscsgrpALT  48142  1neven  48154  2zlidl  48156  2zrngamgm  48161  2zrngagrp  48165  2zrngmmgm  48168  2zrngnmrid  48172  itsclc0  48692  itsclc0b  48693  isthinc  49069  istermc  49121