Theorem elrab2 3674

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461

This theorem is referenced by:  rru  3762  elrabsf  3811  fvmpti  6984  fvmptss2  7011  tfis  7848  elom  7862  oawordeulem  8564  oeeulem  8611  mapfienlem1  9415  mapfienlem3  9417  mapfien  9418  ordtypelem2  9531  ordtypelem3  9532  ordtypelem9  9538  wemapso2lem  9564  inf3lema  9636  oemapvali  9696  tz9.12lem3  9801  cofsmo  10281  enfin2i  10333  fin23lem28  10352  isf32lem6  10370  hsmexlem4  10441  zorn2lem2  10509  pwfseqlem1  10670  pwfseqlem3  10672  nqereu  10941  elz  12588  zsupss  12951  rpnnen1lem5  12995  elrp  13008  repos  13461  wwlktovf  14973  wwlktovf1  14974  wwlktovfo  14975  01sqrexlem1  15259  01sqrexlem2  15260  01sqrexlem6  15264  01sqrexlem7  15265  ello1  15529  elo1  15540  rlimrege0  15593  divalglem2  16412  divalglem4  16413  divalglem5  16414  divalglem9  16418  divalglem10  16419  bitsfzolem  16451  gcdcllem1  16516  gcdcllem2  16517  gcdcllem3  16518  bezoutlem1  16556  bezoutlem3  16558  bezoutlem4  16559  isprm  16690  maxprmfct  16726  phimullem  16796  eulerthlem1  16798  eulerthlem2  16799  hashgcdlem  16805  pclem  16856  pcprecl  16857  pcprendvds  16858  infpn2  16931  prmreclem1  16934  prmreclem2  16935  prmreclem3  16936  prmreclem5  16938  1arith  16945  elgz  16949  4sqlem13  16975  4sqlem17  16979  4sqlem18  16980  vdwnnlem2  17014  vdwnnlem3  17015  ramtlecl  17018  isdrs  18311  istos  18426  islat  18441  isclat  18508  isdlat  18530  istsr  18591  issgrp  18696  ismnddef  18712  gsumvallem2  18810  isgrp  18920  elnmz  19144  gastacl  19290  gastacos  19291  symgfixelq  19412  psgneldm  19482  sylow1lem2  19578  sylow1lem4  19580  sylow2alem1  19596  sylow2alem2  19597  efgsdm  19709  iscmn  19768  iscyg  19858  iscyggen  19859  dprdw  19991  ablfacrplem  20046  ablfacrp  20047  ablfac1c  20052  ablfac1eu  20054  pgpfaclem1  20062  ablfaclem3  20068  ablfac2  20070  issimpg  20073  isrng  20112  issrg  20146  isring  20195  iscrng  20198  isnzr  20472  islring  20498  isrrg  20656  isdomn  20663  isdrng  20691  islmod  20819  islvec  21060  lspsolvlem  21101  lbsextlem1  21117  lbsextlem3  21119  lbsextlem4  21120  islpir  21287  isphl  21586  pjdm  21665  ishil  21676  frlmssuvc1  21752  frlmssuvc2  21753  frlmsslsp  21754  isassa  21814  psrbag  21875  psrbaglefi  21884  psrbagconcl  21885  psrbagleadd1  21886  gsumbagdiaglem  21888  mplelbas  21949  gsummatr01lem1  22591  gsummatr01lem4  22594  gsummatr01  22595  mretopd  23028  neipeltop  23065  isperf  23087  ist0  23256  ist1  23257  ishaus  23258  iscnrm  23259  isreg  23268  isnrm  23271  ispnrm  23275  iscmp  23324  hauscmplem  23342  isconn  23349  conncompss  23369  is1stc  23377  islly  23404  isnlly  23405  dfac14lem  23553  ishmeo  23695  ptcmplem3  23990  ptcmplem4  23991  istmd  24010  istgp  24013  tgpconncompeqg  24048  tgpt0  24055  qustgpopn  24056  istrg  24100  istdrg  24102  istlm  24121  istvc  24128  iscusp  24235  imasdsf1olem  24310  isxms  24384  isms  24386  blcld  24442  prdsxmslem2  24466  isngp  24533  isnrg  24597  isnlm  24612  icccmplem1  24760  icccmplem2  24761  isclm  25013  iscph  25120  isbn  25288  iscms  25295  ivthlem1  25402  ivthlem2  25403  ivthlem3  25404  elovolm  25426  ovolicc2lem2  25469  ovolicc2lem4  25471  ovolicc2lem5  25472  ismbl  25477  dyadmbllem  25550  dyadmbl  25551  ismbf1  25575  isi1f  25625  isibl  25716  isuc1p  26096  ismon1p  26098  radcnvle  26379  abelthlem2  26392  abelthlem7a  26397  atans  26890  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgambdd  26997  wilthlem2  27029  wilthlem3  27030  ftalem3  27035  sqff1o  27142  mpodvdsmulf1o  27154  dvdsmulf1o  27156  lgslem2  27259  lgslem3  27260  lgsfcl2  27264  rpvmasumlem  27448  dchrvmaeq0  27465  dchrisum0re  27474  pntlem3  27570  0elleft  27865  0elright  27866  addsproplem4  27922  addsproplem5  27923  addsproplem6  27924  negsproplem4  27980  negsproplem5  27981  mulsproplem12  28070  precsexlem8  28155  precsexlem9  28156  precsexlem11  28158  elons  28193  sltonold  28200  elreno  28344  axcontlem2  28890  lfgredgge2  29049  uspgredg2vlem  29148  uspgredg2v  29149  usgredg2vlem1  29150  usgredg2vlem2  29151  ushgredgedg  29154  ushgredgedgloop  29156  uhgrspan1  29228  upgrreslem  29229  umgrreslem  29230  isfusgr  29243  nbupgrres  29289  nbusgredgeu0  29293  nbusgrf1o0  29294  uvtxel  29313  uvtxel1  29321  cusgrexilem2  29367  cusgrfilem2  29382  vtxdginducedm1lem4  29468  rgrx0ndm  29519  iswspthn  29777  wwlknon  29785  wspthnon  29786  wwlksn0  29791  wwlksnextfun  29826  wwlksnextinj  29827  wwlksnextsurj  29828  wwlksnextproplem3  29839  clwlkclwwlkflem  29931  clwlkclwwlkfolem  29934  isclwwlkn  29954  clwwlkel  29973  clwwlkf  29974  clwwlkf1  29976  isclwwlknon  30018  s2elclwwlknon2  30031  isfrgr  30187  frgrwopreglem3  30241  frgrwopreglem5lem  30247  frgrwopreglem5  30248  isablo  30473  iscbn  30791  hcau  31111  issh  31135  isch  31149  elcnop  31784  ellnop  31785  elbdop  31787  elhmop  31800  elcnfn  31809  ellnfn  31810  isst  32140  ishst  32141  ela  32266  ischn  32932  isomnd  33015  isslmd  33145  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspn  33187  isorng  33267  ssdifidllem  33417  ssdifidlprm  33419  ssmxidllem  33434  isufd  33501  iscref  33821  isrrext  33977  ispisys  34129  isldsys  34133  isros  34145  issros  34152  oddpwdc  34332  eulerpartleme  34341  eulerpartlemo  34343  eulerpartlemd  34344  eulerpartlemt0  34347  eulerpartlemf  34348  eulerpartlemt  34349  eulerpartlemr  34352  eulerpartlemmf  34353  eulerpartlemgvv  34354  eulerpartlemgs2  34358  eulerpartlemn  34359  elprob  34387  ballotlemelo  34466  ballotleme  34475  bnj1152  34975  bnj1280  34997  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem1  35159  ispconn  35191  issconn  35194  cvmsiota  35245  cvmlift2lem12  35282  fmla1  35355  gonan0  35360  goaln0  35361  gonar  35363  goalr  35365  sategoelfvb  35387  rdgprc0  35757  elwlim  35787  neibastop1  36323  neibastop2lem  36324  neibastop2  36325  topdifinffinlem  37311  pibp19  37378  pibp21  37379  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  isprrngo  38020  rabeqel  38218  toycom  38937  isopos  39144  isoml  39202  isatl  39263  iscvlat  39287  ishlat1  39316  cdlemm10N  41083  dihglblem2N  41259  lcfl1lem  41456  lcfls1lem  41499  mapdordlem1a  41599  mapdordlem1  41601  iscsrg  41929  readvcot  42354  mhphflem  42566  pellqrex  42849  islnm  43048  pwssplit4  43060  islnr  43082  fnlimcnv  45644  stoweidlem14  45991  stoweidlem16  45993  stoweidlem37  46014  stoweidlem48  46025  stoweidlem51  46028  stoweidlem59  46036  salexct  46311  salexct2  46316  salexct3  46319  salgencntex  46320  salgensscntex  46321  ovn0lem  46542  opnvonmbllem1  46609  ovolval5lem2  46630  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  smfresal  46765  smfmullem2  46769  smfpimbor1lem1  46775  smfpimbor1lem2  46776  smfinflem  46794  sprsymrelfo  47459  prproropf1olem1  47465  pairreueq  47472  iseven  47590  isodd  47591  m1expevenALTV  47609  iseven2  47613  isodd3  47614  odd2np1ALTV  47636  opoeALTV  47645  opeoALTV  47646  isgbe  47713  isgbow  47714  isgbo  47715  uspgrlimlem2  47949  uspgrlimlem3  47950  uspgrlimlem4  47951  0nodd  48093  1odd  48094  2nodd  48095  iscmgmALT  48147  issgrpALT  48148  iscsgrpALT  48149  1neven  48161  2zlidl  48163  2zrngamgm  48168  2zrngagrp  48172  2zrngmmgm  48175  2zrngnmrid  48179  itsclc0  48699  itsclc0b  48700  isthinc  49253  istermc  49308