Theorem elrab2 3665

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452

This theorem is referenced by:  rru  3753  elrabsf  3802  fvmpti  6970  fvmptss2  6997  tfis  7834  elom  7848  oawordeulem  8521  oeeulem  8568  mapfienlem1  9363  mapfienlem3  9365  mapfien  9366  ordtypelem2  9479  ordtypelem3  9480  ordtypelem9  9486  wemapso2lem  9512  inf3lema  9584  oemapvali  9644  tz9.12lem3  9749  cofsmo  10229  enfin2i  10281  fin23lem28  10300  isf32lem6  10318  hsmexlem4  10389  zorn2lem2  10457  pwfseqlem1  10618  pwfseqlem3  10620  nqereu  10889  elz  12538  zsupss  12903  rpnnen1lem5  12947  elrp  12960  repos  13414  wwlktovf  14929  wwlktovf1  14930  wwlktovfo  14931  01sqrexlem1  15215  01sqrexlem2  15216  01sqrexlem6  15220  01sqrexlem7  15221  ello1  15488  elo1  15499  rlimrege0  15552  divalglem2  16372  divalglem4  16373  divalglem5  16374  divalglem9  16378  divalglem10  16379  bitsfzolem  16411  gcdcllem1  16476  gcdcllem2  16477  gcdcllem3  16478  bezoutlem1  16516  bezoutlem3  16518  bezoutlem4  16519  isprm  16650  maxprmfct  16686  phimullem  16756  eulerthlem1  16758  eulerthlem2  16759  hashgcdlem  16765  pclem  16816  pcprecl  16817  pcprendvds  16818  infpn2  16891  prmreclem1  16894  prmreclem2  16895  prmreclem3  16896  prmreclem5  16898  1arith  16905  elgz  16909  4sqlem13  16935  4sqlem17  16939  4sqlem18  16940  vdwnnlem2  16974  vdwnnlem3  16975  ramtlecl  16978  isdrs  18269  istos  18384  islat  18399  isclat  18466  isdlat  18488  istsr  18549  issgrp  18654  ismnddef  18670  gsumvallem2  18768  isgrp  18878  elnmz  19102  gastacl  19248  gastacos  19249  symgfixelq  19370  psgneldm  19440  sylow1lem2  19536  sylow1lem4  19538  sylow2alem1  19554  sylow2alem2  19555  efgsdm  19667  iscmn  19726  iscyg  19816  iscyggen  19817  dprdw  19949  ablfacrplem  20004  ablfacrp  20005  ablfac1c  20010  ablfac1eu  20012  pgpfaclem1  20020  ablfaclem3  20026  ablfac2  20028  issimpg  20031  isrng  20070  issrg  20104  isring  20153  iscrng  20156  isnzr  20430  islring  20456  isrrg  20614  isdomn  20621  isdrng  20649  islmod  20777  islvec  21018  lspsolvlem  21059  lbsextlem1  21075  lbsextlem3  21077  lbsextlem4  21078  islpir  21245  isphl  21544  pjdm  21623  ishil  21634  frlmssuvc1  21710  frlmssuvc2  21711  frlmsslsp  21712  isassa  21772  psrbag  21833  psrbaglefi  21842  psrbagconcl  21843  psrbagleadd1  21844  gsumbagdiaglem  21846  mplelbas  21907  gsummatr01lem1  22549  gsummatr01lem4  22552  gsummatr01  22553  mretopd  22986  neipeltop  23023  isperf  23045  ist0  23214  ist1  23215  ishaus  23216  iscnrm  23217  isreg  23226  isnrm  23229  ispnrm  23233  iscmp  23282  hauscmplem  23300  isconn  23307  conncompss  23327  is1stc  23335  islly  23362  isnlly  23363  dfac14lem  23511  ishmeo  23653  ptcmplem3  23948  ptcmplem4  23949  istmd  23968  istgp  23971  tgpconncompeqg  24006  tgpt0  24013  qustgpopn  24014  istrg  24058  istdrg  24060  istlm  24079  istvc  24086  iscusp  24193  imasdsf1olem  24268  isxms  24342  isms  24344  blcld  24400  prdsxmslem2  24424  isngp  24491  isnrg  24555  isnlm  24570  icccmplem1  24718  icccmplem2  24719  isclm  24971  iscph  25077  isbn  25245  iscms  25252  ivthlem1  25359  ivthlem2  25360  ivthlem3  25361  elovolm  25383  ovolicc2lem2  25426  ovolicc2lem4  25428  ovolicc2lem5  25429  ismbl  25434  dyadmbllem  25507  dyadmbl  25508  ismbf1  25532  isi1f  25582  isibl  25673  isuc1p  26053  ismon1p  26055  radcnvle  26336  abelthlem2  26349  abelthlem7a  26354  atans  26847  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem5  26950  lgambdd  26954  wilthlem2  26986  wilthlem3  26987  ftalem3  26992  sqff1o  27099  mpodvdsmulf1o  27111  dvdsmulf1o  27113  lgslem2  27216  lgslem3  27217  lgsfcl2  27221  rpvmasumlem  27405  dchrvmaeq0  27422  dchrisum0re  27431  pntlem3  27527  elleft  27780  elright  27781  elons  28161  elreno  28353  axcontlem2  28899  lfgredgge2  29058  uspgredg2vlem  29157  uspgredg2v  29158  usgredg2vlem1  29159  usgredg2vlem2  29160  ushgredgedg  29163  ushgredgedgloop  29165  uhgrspan1  29237  upgrreslem  29238  umgrreslem  29239  isfusgr  29252  nbupgrres  29298  nbusgredgeu0  29302  nbusgrf1o0  29303  uvtxel  29322  uvtxel1  29330  cusgrexilem2  29376  cusgrfilem2  29391  vtxdginducedm1lem4  29477  rgrx0ndm  29528  iswspthn  29786  wwlknon  29794  wspthnon  29795  wwlksn0  29800  wwlksnextfun  29835  wwlksnextinj  29836  wwlksnextsurj  29837  wwlksnextproplem3  29848  clwlkclwwlkflem  29940  clwlkclwwlkfolem  29943  isclwwlkn  29963  clwwlkel  29982  clwwlkf  29983  clwwlkf1  29985  isclwwlknon  30027  s2elclwwlknon2  30040  isfrgr  30196  frgrwopreglem3  30250  frgrwopreglem5lem  30256  frgrwopreglem5  30257  isablo  30482  iscbn  30800  hcau  31120  issh  31144  isch  31158  elcnop  31793  ellnop  31794  elbdop  31796  elhmop  31809  elcnfn  31818  ellnfn  31819  isst  32149  ishst  32150  ela  32275  ischn  32939  isomnd  33022  isslmd  33162  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem4  33203  elrgspn  33204  isorng  33284  ssdifidllem  33434  ssdifidlprm  33436  ssmxidllem  33451  isufd  33518  iscref  33841  isrrext  33997  ispisys  34149  isldsys  34153  isros  34165  issros  34172  oddpwdc  34352  eulerpartleme  34361  eulerpartlemo  34363  eulerpartlemd  34364  eulerpartlemt0  34367  eulerpartlemf  34368  eulerpartlemt  34369  eulerpartlemr  34372  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgs2  34378  eulerpartlemn  34379  elprob  34407  ballotlemelo  34486  ballotleme  34495  bnj1152  34995  bnj1280  35017  subfacp1lem3  35176  subfacp1lem5  35178  erdszelem1  35185  ispconn  35217  issconn  35220  cvmsiota  35271  cvmlift2lem12  35308  fmla1  35381  gonan0  35386  goaln0  35387  gonar  35389  goalr  35391  sategoelfvb  35413  rdgprc0  35788  elwlim  35818  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  topdifinffinlem  37342  pibp19  37409  pibp21  37410  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  isprrngo  38051  rabeqel  38250  toycom  38973  isopos  39180  isoml  39238  isatl  39299  iscvlat  39323  ishlat1  39352  cdlemm10N  41119  dihglblem2N  41295  lcfl1lem  41492  lcfls1lem  41535  mapdordlem1a  41635  mapdordlem1  41637  iscsrg  41965  readvcot  42359  mhphflem  42591  pellqrex  42874  islnm  43073  pwssplit4  43085  islnr  43107  fnlimcnv  45672  stoweidlem14  46019  stoweidlem16  46021  stoweidlem37  46042  stoweidlem48  46053  stoweidlem51  46056  stoweidlem59  46064  salexct  46339  salexct2  46344  salexct3  46347  salgencntex  46348  salgensscntex  46349  ovn0lem  46570  opnvonmbllem1  46637  ovolval5lem2  46658  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  smfresal  46793  smfmullem2  46797  smfpimbor1lem1  46803  smfpimbor1lem2  46804  smfinflem  46822  sprsymrelfo  47502  prproropf1olem1  47508  pairreueq  47515  iseven  47633  isodd  47634  m1expevenALTV  47652  iseven2  47656  isodd3  47657  odd2np1ALTV  47679  opoeALTV  47688  opeoALTV  47689  isgbe  47756  isgbow  47757  isgbo  47758  uspgrlimlem2  47992  uspgrlimlem3  47993  uspgrlimlem4  47994  0nodd  48162  1odd  48163  2nodd  48164  iscmgmALT  48216  issgrpALT  48217  iscsgrpALT  48218  1neven  48230  2zlidl  48232  2zrngamgm  48237  2zrngagrp  48241  2zrngmmgm  48244  2zrngnmrid  48248  itsclc0  48764  itsclc0b  48765  isthinc  49412  istermc  49467