Theorem elrab2 3632

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 3629	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 276	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433

This theorem is referenced by:  rru  3720  elrabsf  3768  fvmpti  6934  fvmptss2  6962  tfis  7795  elom  7809  oawordeulem  8479  oeeulem  8527  mapfienlem1  9308  mapfienlem3  9310  mapfien  9311  ordtypelem2  9424  ordtypelem3  9425  ordtypelem9  9431  wemapso2lem  9457  inf3lema  9536  oemapvali  9596  tz9.12lem3  9704  cofsmo  10182  enfin2i  10234  fin23lem28  10253  isf32lem6  10271  hsmexlem4  10342  zorn2lem2  10410  pwfseqlem1  10572  pwfseqlem3  10574  nqereu  10843  elz  12517  zsupss  12878  rpnnen1lem5  12922  elrp  12935  repos  13390  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  01sqrexlem1  15195  01sqrexlem2  15196  01sqrexlem6  15200  01sqrexlem7  15201  ello1  15468  elo1  15479  rlimrege0  15532  divalglem2  16355  divalglem4  16356  divalglem5  16357  divalglem9  16361  divalglem10  16362  bitsfzolem  16394  gcdcllem1  16459  gcdcllem2  16460  gcdcllem3  16461  bezoutlem1  16499  bezoutlem3  16501  bezoutlem4  16502  isprm  16633  maxprmfct  16670  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  hashgcdlem  16749  pclem  16800  pcprecl  16801  pcprendvds  16802  infpn2  16875  prmreclem1  16878  prmreclem2  16879  prmreclem3  16880  prmreclem5  16882  1arith  16889  elgz  16893  4sqlem13  16919  4sqlem17  16923  4sqlem18  16924  vdwnnlem2  16958  vdwnnlem3  16959  ramtlecl  16962  isdrs  18258  istos  18373  islat  18390  isclat  18457  isdlat  18479  istsr  18540  ischn  18564  issgrp  18679  ismnddef  18695  gsumvallem2  18793  isgrp  18906  elnmz  19129  gastacl  19275  gastacos  19276  symgfixelq  19399  psgneldm  19469  sylow1lem2  19565  sylow1lem4  19567  sylow2alem1  19583  sylow2alem2  19584  efgsdm  19696  iscmn  19755  iscyg  19845  iscyggen  19846  dprdw  19978  ablfacrplem  20033  ablfacrp  20034  ablfac1c  20039  ablfac1eu  20041  pgpfaclem1  20049  ablfaclem3  20055  ablfac2  20057  issimpg  20060  isomnd  20089  isrng  20126  issrg  20160  isring  20209  iscrng  20212  isnzr  20486  islring  20512  isrrg  20670  isdomn  20677  isdrng  20705  isorng  20833  islmod  20854  islvec  21094  lspsolvlem  21135  lbsextlem1  21151  lbsextlem3  21153  lbsextlem4  21154  islpir  21321  isphl  21603  pjdm  21682  ishil  21693  frlmssuvc1  21769  frlmssuvc2  21770  frlmsslsp  21771  isassa  21831  psrbag  21892  psrbaglefi  21901  psrbagconcl  21902  psrbagleadd1  21903  gsumbagdiaglem  21906  mplelbas  21965  gsummatr01lem1  22638  gsummatr01lem4  22641  gsummatr01  22642  mretopd  23075  neipeltop  23112  isperf  23134  ist0  23303  ist1  23304  ishaus  23305  iscnrm  23306  isreg  23315  isnrm  23318  ispnrm  23322  iscmp  23371  hauscmplem  23389  isconn  23396  conncompss  23416  is1stc  23424  islly  23451  isnlly  23452  dfac14lem  23600  ishmeo  23742  ptcmplem3  24037  ptcmplem4  24038  istmd  24057  istgp  24060  tgpconncompeqg  24095  tgpt0  24102  qustgpopn  24103  istrg  24147  istdrg  24149  istlm  24168  istvc  24175  iscusp  24281  imasdsf1olem  24356  isxms  24430  isms  24432  blcld  24488  prdsxmslem2  24512  isngp  24579  isnrg  24643  isnlm  24658  icccmplem1  24806  icccmplem2  24807  isclm  25049  iscph  25155  isbn  25323  iscms  25330  ivthlem1  25436  ivthlem2  25437  ivthlem3  25438  elovolm  25460  ovolicc2lem2  25503  ovolicc2lem4  25505  ovolicc2lem5  25506  ismbl  25511  dyadmbllem  25584  dyadmbl  25585  ismbf1  25609  isi1f  25659  isibl  25750  isuc1p  26124  ismon1p  26126  radcnvle  26403  abelthlem2  26415  abelthlem7a  26420  atans  26912  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgambdd  27018  wilthlem2  27050  wilthlem3  27051  ftalem3  27056  sqff1o  27163  mpodvdsmulf1o  27175  dvdsmulf1o  27177  lgslem2  27279  lgslem3  27280  lgsfcl2  27284  rpvmasumlem  27468  dchrvmaeq0  27485  dchrisum0re  27494  pntlem3  27590  elleft  27861  elright  27862  elons  28263  elreno  28501  axcontlem2  29052  lfgredgge2  29211  uspgredg2vlem  29310  uspgredg2v  29311  usgredg2vlem1  29312  usgredg2vlem2  29313  ushgredgedg  29316  ushgredgedgloop  29318  uhgrspan1  29390  upgrreslem  29391  umgrreslem  29392  isfusgr  29405  nbupgrres  29451  nbusgredgeu0  29455  nbusgrf1o0  29456  uvtxel  29475  uvtxel1  29483  cusgrexilem2  29529  cusgrfilem2  29543  vtxdginducedm1lem4  29629  rgrx0ndm  29680  iswspthn  29935  wwlknon  29943  wspthnon  29944  wwlksn0  29949  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextsurj  29986  wwlksnextproplem3  29997  clwlkclwwlkflem  30092  clwlkclwwlkfolem  30095  isclwwlkn  30115  clwwlkel  30134  clwwlkf  30135  clwwlkf1  30137  isclwwlknon  30179  s2elclwwlknon2  30192  isfrgr  30348  frgrwopreglem3  30402  frgrwopreglem5lem  30408  frgrwopreglem5  30409  isablo  30635  iscbn  30953  hcau  31273  issh  31297  isch  31311  elcnop  31946  ellnop  31947  elbdop  31949  elhmop  31962  elcnfn  31971  ellnfn  31972  isst  32302  ishst  32303  ela  32428  isslmd  33283  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem4  33326  elrgspn  33327  ssdifidllem  33539  ssdifidlprm  33541  ssmxidllem  33556  isufd  33623  iscref  34028  isrrext  34184  ispisys  34336  isldsys  34340  isros  34352  issros  34359  oddpwdc  34538  eulerpartleme  34547  eulerpartlemo  34549  eulerpartlemd  34550  eulerpartlemt0  34553  eulerpartlemf  34554  eulerpartlemt  34555  eulerpartlemr  34558  eulerpartlemmf  34559  eulerpartlemgvv  34560  eulerpartlemgs2  34564  eulerpartlemn  34565  elprob  34593  ballotlemelo  34672  ballotleme  34681  bnj1152  35180  bnj1280  35202  subfacp1lem3  35410  subfacp1lem5  35412  erdszelem1  35419  ispconn  35451  issconn  35454  cvmsiota  35505  cvmlift2lem12  35542  fmla1  35615  gonan0  35620  goaln0  35621  gonar  35623  goalr  35625  sategoelfvb  35647  rdgprc0  36019  elwlim  36049  neibastop1  36587  neibastop2lem  36588  neibastop2  36589  topdifinffinlem  37709  pibp19  37776  pibp21  37777  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem8  37995  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem18  38005  poimirlem19  38006  poimirlem20  38007  poimirlem21  38008  poimirlem22  38009  isprrngo  38417  rabeqel  38624  toycom  39465  isopos  39672  isoml  39730  isatl  39791  iscvlat  39815  ishlat1  39844  cdlemm10N  41610  dihglblem2N  41786  lcfl1lem  41983  lcfls1lem  42026  mapdordlem1a  42126  mapdordlem1  42128  iscsrg  42456  readvcot  42841  mhphflem  43046  pellqrex  43324  islnm  43522  pwssplit4  43534  islnr  43556  fnlimcnv  46110  stoweidlem14  46457  stoweidlem16  46459  stoweidlem37  46480  stoweidlem48  46491  stoweidlem51  46494  stoweidlem59  46502  salexct  46777  salexct2  46782  salexct3  46785  salgencntex  46786  salgensscntex  46787  ovn0lem  47008  opnvonmbllem1  47075  ovolval5lem2  47096  pimincfltioc  47159  pimdecfgtioo  47160  pimincfltioo  47161  smfresal  47231  smfmullem2  47235  smfpimbor1lem1  47241  smfpimbor1lem2  47242  smfinflem  47260  sprsymrelfo  47972  prproropf1olem1  47978  pairreueq  47985  iseven  48119  isodd  48120  m1expevenALTV  48138  iseven2  48142  isodd3  48143  odd2np1ALTV  48165  opoeALTV  48174  opeoALTV  48175  isgbe  48242  isgbow  48243  isgbo  48244  uspgrlimlem2  48480  uspgrlimlem3  48481  uspgrlimlem4  48482  clnbgrvtxedg  48485  grlimpredg  48489  grlimprclnbgrvtx  48490  grlimgrtrilem1  48492  0nodd  48661  1odd  48662  2nodd  48663  iscmgmALT  48715  issgrpALT  48716  iscsgrpALT  48717  1neven  48729  2zlidl  48731  2zrngamgm  48736  2zrngagrp  48740  2zrngmmgm  48743  2zrngnmrid  48747  itsclc0  49262  itsclc0b  49263  isthinc  49909  istermc  49964