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  27405  0elright  27406  addsproplem4  27458  addsproplem5  27459  addsproplem6  27460  negsproplem4  27508  negsproplem5  27509  mulsproplem12  27586  precsexlem8  27663  precsexlem9  27664  precsexlem11  27666  elons  27683  sltonold  27690  axcontlem2  28254  lfgredgge2  28415  uspgredg2vlem  28511  uspgredg2v  28512  usgredg2vlem1  28513  usgredg2vlem2  28514  ushgredgedg  28517  ushgredgedgloop  28519  uhgrspan1  28591  upgrreslem  28592  umgrreslem  28593  isfusgr  28606  nbupgrres  28652  nbusgredgeu0  28656  nbusgrf1o0  28657  uvtxel  28676  uvtxel1  28684  cusgrexilem2  28730  cusgrfilem2  28744  vtxdginducedm1lem4  28830  rgrx0ndm  28881  iswspthn  29134  wwlknon  29142  wspthnon  29143  wwlksn0  29148  wwlksnextfun  29183  wwlksnextinj  29184  wwlksnextsurj  29185  wwlksnextproplem3  29196  clwlkclwwlkflem  29288  clwlkclwwlkfolem  29291  isclwwlkn  29311  clwwlkel  29330  clwwlkf  29331  clwwlkf1  29333  isclwwlknon  29375  s2elclwwlknon2  29388  isfrgr  29544  frgrwopreglem3  29598  frgrwopreglem5lem  29604  frgrwopreglem5  29605  isablo  29830  iscbn  30148  hcau  30468  issh  30492  isch  30506  elcnop  31141  ellnop  31142  elbdop  31144  elhmop  31157  elcnfn  31166  ellnfn  31167  isst  31497  ishst  31498  ela  31623  isomnd  32250  isslmd  32378  isorng  32448  ssmxidllem  32620  isufd  32663  iscref  32855  isrrext  33011  ispisys  33181  isldsys  33185  isros  33197  issros  33204  oddpwdc  33384  eulerpartleme  33393  eulerpartlemo  33395  eulerpartlemd  33396  eulerpartlemt0  33399  eulerpartlemf  33400  eulerpartlemt  33401  eulerpartlemr  33404  eulerpartlemmf  33405  eulerpartlemgvv  33406  eulerpartlemgs2  33410  eulerpartlemn  33411  elprob  33439  ballotlemelo  33517  ballotleme  33526  bnj1152  34040  bnj1280  34062  subfacp1lem3  34204  subfacp1lem5  34206  erdszelem1  34213  ispconn  34245  issconn  34248  cvmsiota  34299  cvmlift2lem12  34336  fmla1  34409  gonan0  34414  goaln0  34415  gonar  34417  goalr  34419  sategoelfvb  34441  rdgprc0  34796  elwlim  34826  neibastop1  35292  neibastop2lem  35293  neibastop2  35294  topdifinffinlem  36276  pibp19  36343  pibp21  36344  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem8  36544  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem18  36554  poimirlem19  36555  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  isprrngo  36966  rabeqel  37170  toycom  37891  isopos  38098  isoml  38156  isatl  38217  iscvlat  38241  ishlat1  38270  cdlemm10N  40037  dihglblem2N  40213  lcfl1lem  40410  lcfls1lem  40453  mapdordlem1a  40553  mapdordlem1  40555  mhphflem  41216  pellqrex  41665  islnm  41867  pwssplit4  41879  islnr  41901  fnlimcnv  44431  stoweidlem14  44778  stoweidlem16  44780  stoweidlem37  44801  stoweidlem48  44812  stoweidlem51  44815  stoweidlem59  44823  salexct  45098  salexct2  45103  salexct3  45106  salgencntex  45107  salgensscntex  45108  ovn0lem  45329  opnvonmbllem1  45396  ovolval5lem2  45417  pimincfltioc  45480  pimdecfgtioo  45481  pimincfltioo  45482  smfresal  45552  smfmullem2  45556  smfpimbor1lem1  45562  smfpimbor1lem2  45563  smfinflem  45581  sprsymrelfo  46213  prproropf1olem1  46219  pairreueq  46226  iseven  46344  isodd  46345  m1expevenALTV  46363  iseven2  46367  isodd3  46368  odd2np1ALTV  46390  opoeALTV  46399  opeoALTV  46400  isgbe  46467  isgbow  46468  isgbo  46469  0nodd  46628  1odd  46629  2nodd  46630  iscmgmALT  46682  issgrpALT  46683  iscsgrpALT  46684  isrng  46698  1neven  46878  2zlidl  46880  2zrngamgm  46885  2zrngagrp  46889  2zrngmmgm  46892  2zrngnmrid  46896  itsclc0  47505  itsclc0b  47506  isthinc  47689