Theorem elrab2 3637

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431

This theorem is referenced by:  rru  3725  elrabsf  3774  fvmpti  6946  fvmptss2  6974  tfis  7806  elom  7820  oawordeulem  8489  oeeulem  8537  mapfienlem1  9318  mapfienlem3  9320  mapfien  9321  ordtypelem2  9434  ordtypelem3  9435  ordtypelem9  9441  wemapso2lem  9467  inf3lema  9545  oemapvali  9605  tz9.12lem3  9713  cofsmo  10191  enfin2i  10243  fin23lem28  10262  isf32lem6  10280  hsmexlem4  10351  zorn2lem2  10419  pwfseqlem1  10581  pwfseqlem3  10583  nqereu  10852  elz  12526  zsupss  12887  rpnnen1lem5  12931  elrp  12944  repos  13399  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  01sqrexlem1  15204  01sqrexlem2  15205  01sqrexlem6  15209  01sqrexlem7  15210  ello1  15477  elo1  15488  rlimrege0  15541  divalglem2  16364  divalglem4  16365  divalglem5  16366  divalglem9  16370  divalglem10  16371  bitsfzolem  16403  gcdcllem1  16468  gcdcllem2  16469  gcdcllem3  16470  bezoutlem1  16508  bezoutlem3  16510  bezoutlem4  16511  isprm  16642  maxprmfct  16679  phimullem  16749  eulerthlem1  16751  eulerthlem2  16752  hashgcdlem  16758  pclem  16809  pcprecl  16810  pcprendvds  16811  infpn2  16884  prmreclem1  16887  prmreclem2  16888  prmreclem3  16889  prmreclem5  16891  1arith  16898  elgz  16902  4sqlem13  16928  4sqlem17  16932  4sqlem18  16933  vdwnnlem2  16967  vdwnnlem3  16968  ramtlecl  16971  isdrs  18267  istos  18382  islat  18399  isclat  18466  isdlat  18488  istsr  18549  ischn  18573  issgrp  18688  ismnddef  18704  gsumvallem2  18802  isgrp  18915  elnmz  19138  gastacl  19284  gastacos  19285  symgfixelq  19408  psgneldm  19478  sylow1lem2  19574  sylow1lem4  19576  sylow2alem1  19592  sylow2alem2  19593  efgsdm  19705  iscmn  19764  iscyg  19854  iscyggen  19855  dprdw  19987  ablfacrplem  20042  ablfacrp  20043  ablfac1c  20048  ablfac1eu  20050  pgpfaclem1  20058  ablfaclem3  20064  ablfac2  20066  issimpg  20069  isomnd  20098  isrng  20135  issrg  20169  isring  20218  iscrng  20221  isnzr  20491  islring  20517  isrrg  20675  isdomn  20682  isdrng  20710  isorng  20838  islmod  20859  islvec  21099  lspsolvlem  21140  lbsextlem1  21156  lbsextlem3  21158  lbsextlem4  21159  islpir  21326  isphl  21608  pjdm  21687  ishil  21698  frlmssuvc1  21774  frlmssuvc2  21775  frlmsslsp  21776  isassa  21836  psrbag  21897  psrbaglefi  21906  psrbagconcl  21907  psrbagleadd1  21908  gsumbagdiaglem  21910  mplelbas  21969  gsummatr01lem1  22620  gsummatr01lem4  22623  gsummatr01  22624  mretopd  23057  neipeltop  23094  isperf  23116  ist0  23285  ist1  23286  ishaus  23287  iscnrm  23288  isreg  23297  isnrm  23300  ispnrm  23304  iscmp  23353  hauscmplem  23371  isconn  23378  conncompss  23398  is1stc  23406  islly  23433  isnlly  23434  dfac14lem  23582  ishmeo  23724  ptcmplem3  24019  ptcmplem4  24020  istmd  24039  istgp  24042  tgpconncompeqg  24077  tgpt0  24084  qustgpopn  24085  istrg  24129  istdrg  24131  istlm  24150  istvc  24157  iscusp  24263  imasdsf1olem  24338  isxms  24412  isms  24414  blcld  24470  prdsxmslem2  24494  isngp  24561  isnrg  24625  isnlm  24640  icccmplem1  24788  icccmplem2  24789  isclm  25031  iscph  25137  isbn  25305  iscms  25312  ivthlem1  25418  ivthlem2  25419  ivthlem3  25420  elovolm  25442  ovolicc2lem2  25485  ovolicc2lem4  25487  ovolicc2lem5  25488  ismbl  25493  dyadmbllem  25566  dyadmbl  25567  ismbf1  25591  isi1f  25641  isibl  25732  isuc1p  26106  ismon1p  26108  radcnvle  26385  abelthlem2  26397  abelthlem7a  26402  atans  26894  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem5  26996  lgambdd  27000  wilthlem2  27032  wilthlem3  27033  ftalem3  27038  sqff1o  27145  mpodvdsmulf1o  27157  dvdsmulf1o  27159  lgslem2  27261  lgslem3  27262  lgsfcl2  27266  rpvmasumlem  27450  dchrvmaeq0  27467  dchrisum0re  27476  pntlem3  27572  elleft  27843  elright  27844  elons  28245  elreno  28483  axcontlem2  29034  lfgredgge2  29193  uspgredg2vlem  29292  uspgredg2v  29293  usgredg2vlem1  29294  usgredg2vlem2  29295  ushgredgedg  29298  ushgredgedgloop  29300  uhgrspan1  29372  upgrreslem  29373  umgrreslem  29374  isfusgr  29387  nbupgrres  29433  nbusgredgeu0  29437  nbusgrf1o0  29438  uvtxel  29457  uvtxel1  29465  cusgrexilem2  29511  cusgrfilem2  29525  vtxdginducedm1lem4  29611  rgrx0ndm  29662  iswspthn  29917  wwlknon  29925  wspthnon  29926  wwlksn0  29931  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextsurj  29968  wwlksnextproplem3  29979  clwlkclwwlkflem  30074  clwlkclwwlkfolem  30077  isclwwlkn  30097  clwwlkel  30116  clwwlkf  30117  clwwlkf1  30119  isclwwlknon  30161  s2elclwwlknon2  30174  isfrgr  30330  frgrwopreglem3  30384  frgrwopreglem5lem  30390  frgrwopreglem5  30391  isablo  30617  iscbn  30935  hcau  31255  issh  31279  isch  31293  elcnop  31928  ellnop  31929  elbdop  31931  elhmop  31944  elcnfn  31953  ellnfn  31954  isst  32284  ishst  32285  ela  32410  isslmd  33263  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspn  33307  ssdifidllem  33516  ssdifidlprm  33518  ssmxidllem  33533  isufd  33600  iscref  33988  isrrext  34144  ispisys  34296  isldsys  34300  isros  34312  issros  34319  oddpwdc  34498  eulerpartleme  34507  eulerpartlemo  34509  eulerpartlemd  34510  eulerpartlemt0  34513  eulerpartlemf  34514  eulerpartlemt  34515  eulerpartlemr  34518  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgs2  34524  eulerpartlemn  34525  elprob  34553  ballotlemelo  34632  ballotleme  34641  bnj1152  35140  bnj1280  35162  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem1  35373  ispconn  35405  issconn  35408  cvmsiota  35459  cvmlift2lem12  35496  fmla1  35569  gonan0  35574  goaln0  35575  gonar  35577  goalr  35579  sategoelfvb  35601  rdgprc0  35973  elwlim  36003  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  topdifinffinlem  37663  pibp19  37730  pibp21  37731  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  isprrngo  38371  rabeqel  38578  toycom  39419  isopos  39626  isoml  39684  isatl  39745  iscvlat  39769  ishlat1  39798  cdlemm10N  41564  dihglblem2N  41740  lcfl1lem  41937  lcfls1lem  41980  mapdordlem1a  42080  mapdordlem1  42082  iscsrg  42410  readvcot  42796  mhphflem  43029  pellqrex  43307  islnm  43505  pwssplit4  43517  islnr  43539  fnlimcnv  46095  stoweidlem14  46442  stoweidlem16  46444  stoweidlem37  46465  stoweidlem48  46476  stoweidlem51  46479  stoweidlem59  46487  salexct  46762  salexct2  46767  salexct3  46770  salgencntex  46771  salgensscntex  46772  ovn0lem  46993  opnvonmbllem1  47060  ovolval5lem2  47081  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  smfresal  47216  smfmullem2  47220  smfpimbor1lem1  47226  smfpimbor1lem2  47227  smfinflem  47245  sprsymrelfo  47957  prproropf1olem1  47963  pairreueq  47970  iseven  48104  isodd  48105  m1expevenALTV  48123  iseven2  48127  isodd3  48128  odd2np1ALTV  48150  opoeALTV  48159  opeoALTV  48160  isgbe  48227  isgbow  48228  isgbo  48229  uspgrlimlem2  48465  uspgrlimlem3  48466  uspgrlimlem4  48467  clnbgrvtxedg  48470  grlimpredg  48474  grlimprclnbgrvtx  48475  grlimgrtrilem1  48477  0nodd  48646  1odd  48647  2nodd  48648  iscmgmALT  48700  issgrpALT  48701  iscsgrpALT  48702  1neven  48714  2zlidl  48716  2zrngamgm  48721  2zrngagrp  48725  2zrngmmgm  48728  2zrngnmrid  48732  itsclc0  49247  itsclc0b  49248  isthinc  49894  istermc  49949