Theorem elrab2 3638

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432

This theorem is referenced by:  rru  3726  elrabsf  3775  fvmpti  6940  fvmptss2  6968  tfis  7799  elom  7813  oawordeulem  8482  oeeulem  8530  mapfienlem1  9311  mapfienlem3  9313  mapfien  9314  ordtypelem2  9427  ordtypelem3  9428  ordtypelem9  9434  wemapso2lem  9460  inf3lema  9536  oemapvali  9596  tz9.12lem3  9704  cofsmo  10182  enfin2i  10234  fin23lem28  10253  isf32lem6  10271  hsmexlem4  10342  zorn2lem2  10410  pwfseqlem1  10572  pwfseqlem3  10574  nqereu  10843  elz  12517  zsupss  12878  rpnnen1lem5  12922  elrp  12935  repos  13390  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  01sqrexlem1  15195  01sqrexlem2  15196  01sqrexlem6  15200  01sqrexlem7  15201  ello1  15468  elo1  15479  rlimrege0  15532  divalglem2  16355  divalglem4  16356  divalglem5  16357  divalglem9  16361  divalglem10  16362  bitsfzolem  16394  gcdcllem1  16459  gcdcllem2  16460  gcdcllem3  16461  bezoutlem1  16499  bezoutlem3  16501  bezoutlem4  16502  isprm  16633  maxprmfct  16670  phimullem  16740  eulerthlem1  16742  eulerthlem2  16743  hashgcdlem  16749  pclem  16800  pcprecl  16801  pcprendvds  16802  infpn2  16875  prmreclem1  16878  prmreclem2  16879  prmreclem3  16880  prmreclem5  16882  1arith  16889  elgz  16893  4sqlem13  16919  4sqlem17  16923  4sqlem18  16924  vdwnnlem2  16958  vdwnnlem3  16959  ramtlecl  16962  isdrs  18258  istos  18373  islat  18390  isclat  18457  isdlat  18479  istsr  18540  ischn  18564  issgrp  18679  ismnddef  18695  gsumvallem2  18793  isgrp  18906  elnmz  19129  gastacl  19275  gastacos  19276  symgfixelq  19399  psgneldm  19469  sylow1lem2  19565  sylow1lem4  19567  sylow2alem1  19583  sylow2alem2  19584  efgsdm  19696  iscmn  19755  iscyg  19845  iscyggen  19846  dprdw  19978  ablfacrplem  20033  ablfacrp  20034  ablfac1c  20039  ablfac1eu  20041  pgpfaclem1  20049  ablfaclem3  20055  ablfac2  20057  issimpg  20060  isomnd  20089  isrng  20126  issrg  20160  isring  20209  iscrng  20212  isnzr  20482  islring  20508  isrrg  20666  isdomn  20673  isdrng  20701  isorng  20829  islmod  20850  islvec  21091  lspsolvlem  21132  lbsextlem1  21148  lbsextlem3  21150  lbsextlem4  21151  islpir  21318  isphl  21618  pjdm  21697  ishil  21708  frlmssuvc1  21784  frlmssuvc2  21785  frlmsslsp  21786  isassa  21846  psrbag  21907  psrbaglefi  21916  psrbagconcl  21917  psrbagleadd1  21918  gsumbagdiaglem  21920  mplelbas  21979  gsummatr01lem1  22630  gsummatr01lem4  22633  gsummatr01  22634  mretopd  23067  neipeltop  23104  isperf  23126  ist0  23295  ist1  23296  ishaus  23297  iscnrm  23298  isreg  23307  isnrm  23310  ispnrm  23314  iscmp  23363  hauscmplem  23381  isconn  23388  conncompss  23408  is1stc  23416  islly  23443  isnlly  23444  dfac14lem  23592  ishmeo  23734  ptcmplem3  24029  ptcmplem4  24030  istmd  24049  istgp  24052  tgpconncompeqg  24087  tgpt0  24094  qustgpopn  24095  istrg  24139  istdrg  24141  istlm  24160  istvc  24167  iscusp  24273  imasdsf1olem  24348  isxms  24422  isms  24424  blcld  24480  prdsxmslem2  24504  isngp  24571  isnrg  24635  isnlm  24650  icccmplem1  24798  icccmplem2  24799  isclm  25041  iscph  25147  isbn  25315  iscms  25322  ivthlem1  25428  ivthlem2  25429  ivthlem3  25430  elovolm  25452  ovolicc2lem2  25495  ovolicc2lem4  25497  ovolicc2lem5  25498  ismbl  25503  dyadmbllem  25576  dyadmbl  25577  ismbf1  25601  isi1f  25651  isibl  25742  isuc1p  26116  ismon1p  26118  radcnvle  26398  abelthlem2  26410  abelthlem7a  26415  atans  26907  lgamgulmlem2  27007  lgamgulmlem3  27008  lgamgulmlem5  27010  lgambdd  27014  wilthlem2  27046  wilthlem3  27047  ftalem3  27052  sqff1o  27159  mpodvdsmulf1o  27171  dvdsmulf1o  27173  lgslem2  27275  lgslem3  27276  lgsfcl2  27280  rpvmasumlem  27464  dchrvmaeq0  27481  dchrisum0re  27490  pntlem3  27586  elleft  27857  elright  27858  elons  28259  elreno  28497  axcontlem2  29048  lfgredgge2  29207  uspgredg2vlem  29306  uspgredg2v  29307  usgredg2vlem1  29308  usgredg2vlem2  29309  ushgredgedg  29312  ushgredgedgloop  29314  uhgrspan1  29386  upgrreslem  29387  umgrreslem  29388  isfusgr  29401  nbupgrres  29447  nbusgredgeu0  29451  nbusgrf1o0  29452  uvtxel  29471  uvtxel1  29479  cusgrexilem2  29525  cusgrfilem2  29540  vtxdginducedm1lem4  29626  rgrx0ndm  29677  iswspthn  29932  wwlknon  29940  wspthnon  29941  wwlksn0  29946  wwlksnextfun  29981  wwlksnextinj  29982  wwlksnextsurj  29983  wwlksnextproplem3  29994  clwlkclwwlkflem  30089  clwlkclwwlkfolem  30092  isclwwlkn  30112  clwwlkel  30131  clwwlkf  30132  clwwlkf1  30134  isclwwlknon  30176  s2elclwwlknon2  30189  isfrgr  30345  frgrwopreglem3  30399  frgrwopreglem5lem  30405  frgrwopreglem5  30406  isablo  30632  iscbn  30950  hcau  31270  issh  31294  isch  31308  elcnop  31943  ellnop  31944  elbdop  31946  elhmop  31959  elcnfn  31968  ellnfn  31969  isst  32299  ishst  32300  ela  32425  isslmd  33278  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspn  33322  ssdifidllem  33531  ssdifidlprm  33533  ssmxidllem  33548  isufd  33615  iscref  34004  isrrext  34160  ispisys  34312  isldsys  34316  isros  34328  issros  34335  oddpwdc  34514  eulerpartleme  34523  eulerpartlemo  34525  eulerpartlemd  34526  eulerpartlemt0  34529  eulerpartlemf  34530  eulerpartlemt  34531  eulerpartlemr  34534  eulerpartlemmf  34535  eulerpartlemgvv  34536  eulerpartlemgs2  34540  eulerpartlemn  34541  elprob  34569  ballotlemelo  34648  ballotleme  34657  bnj1152  35156  bnj1280  35178  subfacp1lem3  35380  subfacp1lem5  35382  erdszelem1  35389  ispconn  35421  issconn  35424  cvmsiota  35475  cvmlift2lem12  35512  fmla1  35585  gonan0  35590  goaln0  35591  gonar  35593  goalr  35595  sategoelfvb  35617  rdgprc0  35989  elwlim  36019  neibastop1  36557  neibastop2lem  36558  neibastop2  36559  topdifinffinlem  37677  pibp19  37744  pibp21  37745  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem8  37963  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  isprrngo  38385  rabeqel  38592  toycom  39433  isopos  39640  isoml  39698  isatl  39759  iscvlat  39783  ishlat1  39812  cdlemm10N  41578  dihglblem2N  41754  lcfl1lem  41951  lcfls1lem  41994  mapdordlem1a  42094  mapdordlem1  42096  iscsrg  42424  readvcot  42810  mhphflem  43043  pellqrex  43325  islnm  43523  pwssplit4  43535  islnr  43557  fnlimcnv  46113  stoweidlem14  46460  stoweidlem16  46462  stoweidlem37  46483  stoweidlem48  46494  stoweidlem51  46497  stoweidlem59  46505  salexct  46780  salexct2  46785  salexct3  46788  salgencntex  46789  salgensscntex  46790  ovn0lem  47011  opnvonmbllem1  47078  ovolval5lem2  47099  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  smfresal  47234  smfmullem2  47238  smfpimbor1lem1  47244  smfpimbor1lem2  47245  smfinflem  47263  sprsymrelfo  47969  prproropf1olem1  47975  pairreueq  47982  iseven  48116  isodd  48117  m1expevenALTV  48135  iseven2  48139  isodd3  48140  odd2np1ALTV  48162  opoeALTV  48171  opeoALTV  48172  isgbe  48239  isgbow  48240  isgbo  48241  uspgrlimlem2  48477  uspgrlimlem3  48478  uspgrlimlem4  48479  clnbgrvtxedg  48482  grlimpredg  48486  grlimprclnbgrvtx  48487  grlimgrtrilem1  48489  0nodd  48658  1odd  48659  2nodd  48660  iscmgmALT  48712  issgrpALT  48713  iscsgrpALT  48714  1neven  48726  2zlidl  48728  2zrngamgm  48733  2zrngagrp  48737  2zrngmmgm  48740  2zrngnmrid  48744  itsclc0  49259  itsclc0b  49260  isthinc  49906  istermc  49961