Theorem elrab2 3687

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {crab 3433

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477

This theorem is referenced by:  rru  3776  elrabsf  3826  fvmpti  6998  fvmptss2  7024  tfis  7844  elom  7858  oawordeulem  8554  oeeulem  8601  mapfienlem1  9400  mapfienlem3  9402  mapfien  9403  ordtypelem2  9514  ordtypelem3  9515  ordtypelem9  9521  wemapso2lem  9547  inf3lema  9619  oemapvali  9679  tz9.12lem3  9784  cofsmo  10264  enfin2i  10316  fin23lem28  10335  isf32lem6  10353  hsmexlem4  10424  zorn2lem2  10492  pwfseqlem1  10653  pwfseqlem3  10655  nqereu  10924  elz  12560  zsupss  12921  rpnnen1lem5  12965  elrp  12976  repos  13423  wwlktovf  14907  wwlktovf1  14908  wwlktovfo  14909  01sqrexlem1  15189  01sqrexlem2  15190  01sqrexlem6  15194  01sqrexlem7  15195  ello1  15459  elo1  15470  rlimrege0  15523  divalglem2  16338  divalglem4  16339  divalglem5  16340  divalglem9  16344  divalglem10  16345  bitsfzolem  16375  gcdcllem1  16440  gcdcllem2  16441  gcdcllem3  16442  bezoutlem1  16481  bezoutlem3  16483  bezoutlem4  16484  isprm  16610  maxprmfct  16646  phimullem  16712  eulerthlem1  16714  eulerthlem2  16715  hashgcdlem  16721  pclem  16771  pcprecl  16772  pcprendvds  16773  infpn2  16846  prmreclem1  16849  prmreclem2  16850  prmreclem3  16851  prmreclem5  16853  1arith  16860  elgz  16864  4sqlem13  16890  4sqlem17  16894  4sqlem18  16895  vdwnnlem2  16929  vdwnnlem3  16930  ramtlecl  16933  isdrs  18254  istos  18371  islat  18386  isclat  18453  isdlat  18475  istsr  18536  issgrp  18611  ismnddef  18627  gsumvallem2  18715  isgrp  18825  elnmz  19043  gastacl  19173  gastacos  19174  symgfixelq  19301  psgneldm  19371  sylow1lem2  19467  sylow1lem4  19469  sylow2alem1  19485  sylow2alem2  19486  efgsdm  19598  iscmn  19657  iscyg  19747  iscyggen  19748  dprdw  19880  ablfacrplem  19935  ablfacrp  19936  ablfac1c  19941  ablfac1eu  19943  pgpfaclem1  19951  ablfaclem3  19957  ablfac2  19959  issimpg  19962  issrg  20011  isring  20060  iscrng  20063  isnzr  20293  islring  20310  isdrng  20361  islmod  20475  islvec  20715  lspsolvlem  20755  lbsextlem1  20771  lbsextlem3  20773  lbsextlem4  20774  islpir  20887  isrrg  20904  isdomn  20910  isphl  21181  pjdm  21262  ishil  21273  frlmssuvc1  21349  frlmssuvc2  21350  frlmsslsp  21351  isassa  21411  psrbag  21470  psrbaglefi  21485  psrbaglefiOLD  21486  psrbagconcl  21487  psrbagconclOLD  21488  psrbagconf1oOLD  21490  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  mplelbas  21550  gsummatr01lem1  22157  gsummatr01lem4  22160  gsummatr01  22161  mretopd  22596  neipeltop  22633  isperf  22655  ist0  22824  ist1  22825  ishaus  22826  iscnrm  22827  isreg  22836  isnrm  22839  ispnrm  22843  iscmp  22892  hauscmplem  22910  isconn  22917  conncompss  22937  is1stc  22945  islly  22972  isnlly  22973  dfac14lem  23121  ishmeo  23263  ptcmplem3  23558  ptcmplem4  23559  istmd  23578  istgp  23581  tgpconncompeqg  23616  tgpt0  23623  qustgpopn  23624  istrg  23668  istdrg  23670  istlm  23689  istvc  23696  iscusp  23804  imasdsf1olem  23879  isxms  23953  isms  23955  blcld  24014  prdsxmslem2  24038  isngp  24105  isnrg  24177  isnlm  24192  icccmplem1  24338  icccmplem2  24339  isclm  24580  iscph  24687  isbn  24855  iscms  24862  ivthlem1  24968  ivthlem2  24969  ivthlem3  24970  elovolm  24992  ovolicc2lem2  25035  ovolicc2lem4  25037  ovolicc2lem5  25038  ismbl  25043  dyadmbllem  25116  dyadmbl  25117  ismbf1  25141  isi1f  25191  isibl  25283  isuc1p  25658  ismon1p  25660  radcnvle  25932  abelthlem2  25944  abelthlem7a  25949  atans  26435  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem5  26537  lgambdd  26541  wilthlem2  26573  wilthlem3  26574  ftalem3  26579  sqff1o  26686  dvdsmulf1o  26698  lgslem2  26801  lgslem3  26802  lgsfcl2  26806  rpvmasumlem  26990  dchrvmaeq0  27007  dchrisum0re  27016  pntlem3  27112  0elleft  27403  0elright  27404  addsproplem4  27456  addsproplem5  27457  addsproplem6  27458  negsproplem4  27505  negsproplem5  27506  mulsproplem12  27583  precsexlem8  27660  precsexlem9  27661  precsexlem11  27663  axcontlem2  28223  lfgredgge2  28384  uspgredg2vlem  28480  uspgredg2v  28481  usgredg2vlem1  28482  usgredg2vlem2  28483  ushgredgedg  28486  ushgredgedgloop  28488  uhgrspan1  28560  upgrreslem  28561  umgrreslem  28562  isfusgr  28575  nbupgrres  28621  nbusgredgeu0  28625  nbusgrf1o0  28626  uvtxel  28645  uvtxel1  28653  cusgrexilem2  28699  cusgrfilem2  28713  vtxdginducedm1lem4  28799  rgrx0ndm  28850  iswspthn  29103  wwlknon  29111  wspthnon  29112  wwlksn0  29117  wwlksnextfun  29152  wwlksnextinj  29153  wwlksnextsurj  29154  wwlksnextproplem3  29165  clwlkclwwlkflem  29257  clwlkclwwlkfolem  29260  isclwwlkn  29280  clwwlkel  29299  clwwlkf  29300  clwwlkf1  29302  isclwwlknon  29344  s2elclwwlknon2  29357  isfrgr  29513  frgrwopreglem3  29567  frgrwopreglem5lem  29573  frgrwopreglem5  29574  isablo  29799  iscbn  30117  hcau  30437  issh  30461  isch  30475  elcnop  31110  ellnop  31111  elbdop  31113  elhmop  31126  elcnfn  31135  ellnfn  31136  isst  31466  ishst  31467  ela  31592  isomnd  32219  isslmd  32347  isorng  32417  ssmxidllem  32589  isufd  32632  iscref  32824  isrrext  32980  ispisys  33150  isldsys  33154  isros  33166  issros  33173  oddpwdc  33353  eulerpartleme  33362  eulerpartlemo  33364  eulerpartlemd  33365  eulerpartlemt0  33368  eulerpartlemf  33369  eulerpartlemt  33370  eulerpartlemr  33373  eulerpartlemmf  33374  eulerpartlemgvv  33375  eulerpartlemgs2  33379  eulerpartlemn  33380  elprob  33408  ballotlemelo  33486  ballotleme  33495  bnj1152  34009  bnj1280  34031  subfacp1lem3  34173  subfacp1lem5  34175  erdszelem1  34182  ispconn  34214  issconn  34217  cvmsiota  34268  cvmlift2lem12  34305  fmla1  34378  gonan0  34383  goaln0  34384  gonar  34386  goalr  34388  sategoelfvb  34410  rdgprc0  34765  elwlim  34795  neibastop1  35244  neibastop2lem  35245  neibastop2  35246  topdifinffinlem  36228  pibp19  36295  pibp21  36296  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem8  36496  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem18  36506  poimirlem19  36507  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  isprrngo  36918  rabeqel  37122  toycom  37843  isopos  38050  isoml  38108  isatl  38169  iscvlat  38193  ishlat1  38222  cdlemm10N  39989  dihglblem2N  40165  lcfl1lem  40362  lcfls1lem  40405  mapdordlem1a  40505  mapdordlem1  40507  mhphflem  41168  pellqrex  41617  islnm  41819  pwssplit4  41831  islnr  41853  fnlimcnv  44383  stoweidlem14  44730  stoweidlem16  44732  stoweidlem37  44753  stoweidlem48  44764  stoweidlem51  44767  stoweidlem59  44775  salexct  45050  salexct2  45055  salexct3  45058  salgencntex  45059  salgensscntex  45060  ovn0lem  45281  opnvonmbllem1  45348  ovolval5lem2  45369  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  smfresal  45504  smfmullem2  45508  smfpimbor1lem1  45514  smfpimbor1lem2  45515  smfinflem  45533  sprsymrelfo  46165  prproropf1olem1  46171  pairreueq  46178  iseven  46296  isodd  46297  m1expevenALTV  46315  iseven2  46319  isodd3  46320  odd2np1ALTV  46342  opoeALTV  46351  opeoALTV  46352  isgbe  46419  isgbow  46420  isgbo  46421  0nodd  46580  1odd  46581  2nodd  46582  iscmgmALT  46634  issgrpALT  46635  iscsgrpALT  46636  isrng  46650  1neven  46830  2zlidl  46832  2zrngamgm  46837  2zrngagrp  46841  2zrngmmgm  46844  2zrngnmrid  46848  itsclc0  47457  itsclc0b  47458  isthinc  47641