Theorem elrab2 3659

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446

This theorem is referenced by:  rru  3747  elrabsf  3796  fvmpti  6949  fvmptss2  6976  tfis  7811  elom  7825  oawordeulem  8495  oeeulem  8542  mapfienlem1  9332  mapfienlem3  9334  mapfien  9335  ordtypelem2  9448  ordtypelem3  9449  ordtypelem9  9455  wemapso2lem  9481  inf3lema  9553  oemapvali  9613  tz9.12lem3  9718  cofsmo  10198  enfin2i  10250  fin23lem28  10269  isf32lem6  10287  hsmexlem4  10358  zorn2lem2  10426  pwfseqlem1  10587  pwfseqlem3  10589  nqereu  10858  elz  12507  zsupss  12872  rpnnen1lem5  12916  elrp  12929  repos  13383  wwlktovf  14898  wwlktovf1  14899  wwlktovfo  14900  01sqrexlem1  15184  01sqrexlem2  15185  01sqrexlem6  15189  01sqrexlem7  15190  ello1  15457  elo1  15468  rlimrege0  15521  divalglem2  16341  divalglem4  16342  divalglem5  16343  divalglem9  16347  divalglem10  16348  bitsfzolem  16380  gcdcllem1  16445  gcdcllem2  16446  gcdcllem3  16447  bezoutlem1  16485  bezoutlem3  16487  bezoutlem4  16488  isprm  16619  maxprmfct  16655  phimullem  16725  eulerthlem1  16727  eulerthlem2  16728  hashgcdlem  16734  pclem  16785  pcprecl  16786  pcprendvds  16787  infpn2  16860  prmreclem1  16863  prmreclem2  16864  prmreclem3  16865  prmreclem5  16867  1arith  16874  elgz  16878  4sqlem13  16904  4sqlem17  16908  4sqlem18  16909  vdwnnlem2  16943  vdwnnlem3  16944  ramtlecl  16947  isdrs  18238  istos  18353  islat  18368  isclat  18435  isdlat  18457  istsr  18518  issgrp  18623  ismnddef  18639  gsumvallem2  18737  isgrp  18847  elnmz  19071  gastacl  19217  gastacos  19218  symgfixelq  19339  psgneldm  19409  sylow1lem2  19505  sylow1lem4  19507  sylow2alem1  19523  sylow2alem2  19524  efgsdm  19636  iscmn  19695  iscyg  19785  iscyggen  19786  dprdw  19918  ablfacrplem  19973  ablfacrp  19974  ablfac1c  19979  ablfac1eu  19981  pgpfaclem1  19989  ablfaclem3  19995  ablfac2  19997  issimpg  20000  isrng  20039  issrg  20073  isring  20122  iscrng  20125  isnzr  20399  islring  20425  isrrg  20583  isdomn  20590  isdrng  20618  islmod  20746  islvec  20987  lspsolvlem  21028  lbsextlem1  21044  lbsextlem3  21046  lbsextlem4  21047  islpir  21214  isphl  21513  pjdm  21592  ishil  21603  frlmssuvc1  21679  frlmssuvc2  21680  frlmsslsp  21681  isassa  21741  psrbag  21802  psrbaglefi  21811  psrbagconcl  21812  psrbagleadd1  21813  gsumbagdiaglem  21815  mplelbas  21876  gsummatr01lem1  22518  gsummatr01lem4  22521  gsummatr01  22522  mretopd  22955  neipeltop  22992  isperf  23014  ist0  23183  ist1  23184  ishaus  23185  iscnrm  23186  isreg  23195  isnrm  23198  ispnrm  23202  iscmp  23251  hauscmplem  23269  isconn  23276  conncompss  23296  is1stc  23304  islly  23331  isnlly  23332  dfac14lem  23480  ishmeo  23622  ptcmplem3  23917  ptcmplem4  23918  istmd  23937  istgp  23940  tgpconncompeqg  23975  tgpt0  23982  qustgpopn  23983  istrg  24027  istdrg  24029  istlm  24048  istvc  24055  iscusp  24162  imasdsf1olem  24237  isxms  24311  isms  24313  blcld  24369  prdsxmslem2  24393  isngp  24460  isnrg  24524  isnlm  24539  icccmplem1  24687  icccmplem2  24688  isclm  24940  iscph  25046  isbn  25214  iscms  25221  ivthlem1  25328  ivthlem2  25329  ivthlem3  25330  elovolm  25352  ovolicc2lem2  25395  ovolicc2lem4  25397  ovolicc2lem5  25398  ismbl  25403  dyadmbllem  25476  dyadmbl  25477  ismbf1  25501  isi1f  25551  isibl  25642  isuc1p  26022  ismon1p  26024  radcnvle  26305  abelthlem2  26318  abelthlem7a  26323  atans  26816  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem5  26919  lgambdd  26923  wilthlem2  26955  wilthlem3  26956  ftalem3  26961  sqff1o  27068  mpodvdsmulf1o  27080  dvdsmulf1o  27082  lgslem2  27185  lgslem3  27186  lgsfcl2  27190  rpvmasumlem  27374  dchrvmaeq0  27391  dchrisum0re  27400  pntlem3  27496  elleft  27749  elright  27750  elons  28130  elreno  28322  axcontlem2  28868  lfgredgge2  29027  uspgredg2vlem  29126  uspgredg2v  29127  usgredg2vlem1  29128  usgredg2vlem2  29129  ushgredgedg  29132  ushgredgedgloop  29134  uhgrspan1  29206  upgrreslem  29207  umgrreslem  29208  isfusgr  29221  nbupgrres  29267  nbusgredgeu0  29271  nbusgrf1o0  29272  uvtxel  29291  uvtxel1  29299  cusgrexilem2  29345  cusgrfilem2  29360  vtxdginducedm1lem4  29446  rgrx0ndm  29497  iswspthn  29752  wwlknon  29760  wspthnon  29761  wwlksn0  29766  wwlksnextfun  29801  wwlksnextinj  29802  wwlksnextsurj  29803  wwlksnextproplem3  29814  clwlkclwwlkflem  29906  clwlkclwwlkfolem  29909  isclwwlkn  29929  clwwlkel  29948  clwwlkf  29949  clwwlkf1  29951  isclwwlknon  29993  s2elclwwlknon2  30006  isfrgr  30162  frgrwopreglem3  30216  frgrwopreglem5lem  30222  frgrwopreglem5  30223  isablo  30448  iscbn  30766  hcau  31086  issh  31110  isch  31124  elcnop  31759  ellnop  31760  elbdop  31762  elhmop  31775  elcnfn  31784  ellnfn  31785  isst  32115  ishst  32116  ela  32241  ischn  32905  isomnd  32988  isslmd  33128  elrgspnlem1  33166  elrgspnlem2  33167  elrgspnlem4  33169  elrgspn  33170  isorng  33250  ssdifidllem  33400  ssdifidlprm  33402  ssmxidllem  33417  isufd  33484  iscref  33807  isrrext  33963  ispisys  34115  isldsys  34119  isros  34131  issros  34138  oddpwdc  34318  eulerpartleme  34327  eulerpartlemo  34329  eulerpartlemd  34330  eulerpartlemt0  34333  eulerpartlemf  34334  eulerpartlemt  34335  eulerpartlemr  34338  eulerpartlemmf  34339  eulerpartlemgvv  34340  eulerpartlemgs2  34344  eulerpartlemn  34345  elprob  34373  ballotlemelo  34452  ballotleme  34461  bnj1152  34961  bnj1280  34983  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem1  35151  ispconn  35183  issconn  35186  cvmsiota  35237  cvmlift2lem12  35274  fmla1  35347  gonan0  35352  goaln0  35353  gonar  35355  goalr  35357  sategoelfvb  35379  rdgprc0  35754  elwlim  35784  neibastop1  36320  neibastop2lem  36321  neibastop2  36322  topdifinffinlem  37308  pibp19  37375  pibp21  37376  poimirlem5  37592  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem10  37597  poimirlem11  37598  poimirlem12  37599  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem18  37605  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  isprrngo  38017  rabeqel  38216  toycom  38939  isopos  39146  isoml  39204  isatl  39265  iscvlat  39289  ishlat1  39318  cdlemm10N  41085  dihglblem2N  41261  lcfl1lem  41458  lcfls1lem  41501  mapdordlem1a  41601  mapdordlem1  41603  iscsrg  41931  readvcot  42325  mhphflem  42557  pellqrex  42840  islnm  43039  pwssplit4  43051  islnr  43073  fnlimcnv  45638  stoweidlem14  45985  stoweidlem16  45987  stoweidlem37  46008  stoweidlem48  46019  stoweidlem51  46022  stoweidlem59  46030  salexct  46305  salexct2  46310  salexct3  46313  salgencntex  46314  salgensscntex  46315  ovn0lem  46536  opnvonmbllem1  46603  ovolval5lem2  46624  pimincfltioc  46687  pimdecfgtioo  46688  pimincfltioo  46689  smfresal  46759  smfmullem2  46763  smfpimbor1lem1  46769  smfpimbor1lem2  46770  smfinflem  46788  sprsymrelfo  47471  prproropf1olem1  47477  pairreueq  47484  iseven  47602  isodd  47603  m1expevenALTV  47621  iseven2  47625  isodd3  47626  odd2np1ALTV  47648  opoeALTV  47657  opeoALTV  47658  isgbe  47725  isgbow  47726  isgbo  47727  uspgrlimlem2  47961  uspgrlimlem3  47962  uspgrlimlem4  47963  0nodd  48131  1odd  48132  2nodd  48133  iscmgmALT  48185  issgrpALT  48186  iscsgrpALT  48187  1neven  48199  2zlidl  48201  2zrngamgm  48206  2zrngagrp  48210  2zrngmmgm  48213  2zrngnmrid  48217  itsclc0  48733  itsclc0b  48734  isthinc  49381  istermc  49436