Theorem elrab2 3649

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442

This theorem is referenced by:  rru  3737  elrabsf  3786  fvmpti  6940  fvmptss2  6967  tfis  7797  elom  7811  oawordeulem  8481  oeeulem  8529  mapfienlem1  9308  mapfienlem3  9310  mapfien  9311  ordtypelem2  9424  ordtypelem3  9425  ordtypelem9  9431  wemapso2lem  9457  inf3lema  9533  oemapvali  9593  tz9.12lem3  9701  cofsmo  10179  enfin2i  10231  fin23lem28  10250  isf32lem6  10268  hsmexlem4  10339  zorn2lem2  10407  pwfseqlem1  10569  pwfseqlem3  10571  nqereu  10840  elz  12490  zsupss  12850  rpnnen1lem5  12894  elrp  12907  repos  13362  wwlktovf  14879  wwlktovf1  14880  wwlktovfo  14881  01sqrexlem1  15165  01sqrexlem2  15166  01sqrexlem6  15170  01sqrexlem7  15171  ello1  15438  elo1  15449  rlimrege0  15502  divalglem2  16322  divalglem4  16323  divalglem5  16324  divalglem9  16328  divalglem10  16329  bitsfzolem  16361  gcdcllem1  16426  gcdcllem2  16427  gcdcllem3  16428  bezoutlem1  16466  bezoutlem3  16468  bezoutlem4  16469  isprm  16600  maxprmfct  16636  phimullem  16706  eulerthlem1  16708  eulerthlem2  16709  hashgcdlem  16715  pclem  16766  pcprecl  16767  pcprendvds  16768  infpn2  16841  prmreclem1  16844  prmreclem2  16845  prmreclem3  16846  prmreclem5  16848  1arith  16855  elgz  16859  4sqlem13  16885  4sqlem17  16889  4sqlem18  16890  vdwnnlem2  16924  vdwnnlem3  16925  ramtlecl  16928  isdrs  18224  istos  18339  islat  18356  isclat  18423  isdlat  18445  istsr  18506  ischn  18530  issgrp  18645  ismnddef  18661  gsumvallem2  18759  isgrp  18869  elnmz  19092  gastacl  19238  gastacos  19239  symgfixelq  19362  psgneldm  19432  sylow1lem2  19528  sylow1lem4  19530  sylow2alem1  19546  sylow2alem2  19547  efgsdm  19659  iscmn  19718  iscyg  19808  iscyggen  19809  dprdw  19941  ablfacrplem  19996  ablfacrp  19997  ablfac1c  20002  ablfac1eu  20004  pgpfaclem1  20012  ablfaclem3  20018  ablfac2  20020  issimpg  20023  isomnd  20052  isrng  20089  issrg  20123  isring  20172  iscrng  20175  isnzr  20447  islring  20473  isrrg  20631  isdomn  20638  isdrng  20666  isorng  20794  islmod  20815  islvec  21056  lspsolvlem  21097  lbsextlem1  21113  lbsextlem3  21115  lbsextlem4  21116  islpir  21283  isphl  21583  pjdm  21662  ishil  21673  frlmssuvc1  21749  frlmssuvc2  21750  frlmsslsp  21751  isassa  21811  psrbag  21873  psrbaglefi  21882  psrbagconcl  21883  psrbagleadd1  21884  gsumbagdiaglem  21886  mplelbas  21946  gsummatr01lem1  22599  gsummatr01lem4  22602  gsummatr01  22603  mretopd  23036  neipeltop  23073  isperf  23095  ist0  23264  ist1  23265  ishaus  23266  iscnrm  23267  isreg  23276  isnrm  23279  ispnrm  23283  iscmp  23332  hauscmplem  23350  isconn  23357  conncompss  23377  is1stc  23385  islly  23412  isnlly  23413  dfac14lem  23561  ishmeo  23703  ptcmplem3  23998  ptcmplem4  23999  istmd  24018  istgp  24021  tgpconncompeqg  24056  tgpt0  24063  qustgpopn  24064  istrg  24108  istdrg  24110  istlm  24129  istvc  24136  iscusp  24242  imasdsf1olem  24317  isxms  24391  isms  24393  blcld  24449  prdsxmslem2  24473  isngp  24540  isnrg  24604  isnlm  24619  icccmplem1  24767  icccmplem2  24768  isclm  25020  iscph  25126  isbn  25294  iscms  25301  ivthlem1  25408  ivthlem2  25409  ivthlem3  25410  elovolm  25432  ovolicc2lem2  25475  ovolicc2lem4  25477  ovolicc2lem5  25478  ismbl  25483  dyadmbllem  25556  dyadmbl  25557  ismbf1  25581  isi1f  25631  isibl  25722  isuc1p  26102  ismon1p  26104  radcnvle  26385  abelthlem2  26398  abelthlem7a  26403  atans  26896  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem5  26999  lgambdd  27003  wilthlem2  27035  wilthlem3  27036  ftalem3  27041  sqff1o  27148  mpodvdsmulf1o  27160  dvdsmulf1o  27162  lgslem2  27265  lgslem3  27266  lgsfcl2  27270  rpvmasumlem  27454  dchrvmaeq0  27471  dchrisum0re  27480  pntlem3  27576  elleft  27847  elright  27848  elons  28249  elreno  28487  axcontlem2  29038  lfgredgge2  29197  uspgredg2vlem  29296  uspgredg2v  29297  usgredg2vlem1  29298  usgredg2vlem2  29299  ushgredgedg  29302  ushgredgedgloop  29304  uhgrspan1  29376  upgrreslem  29377  umgrreslem  29378  isfusgr  29391  nbupgrres  29437  nbusgredgeu0  29441  nbusgrf1o0  29442  uvtxel  29461  uvtxel1  29469  cusgrexilem2  29515  cusgrfilem2  29530  vtxdginducedm1lem4  29616  rgrx0ndm  29667  iswspthn  29922  wwlknon  29930  wspthnon  29931  wwlksn0  29936  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextsurj  29973  wwlksnextproplem3  29984  clwlkclwwlkflem  30079  clwlkclwwlkfolem  30082  isclwwlkn  30102  clwwlkel  30121  clwwlkf  30122  clwwlkf1  30124  isclwwlknon  30166  s2elclwwlknon2  30179  isfrgr  30335  frgrwopreglem3  30389  frgrwopreglem5lem  30395  frgrwopreglem5  30396  isablo  30621  iscbn  30939  hcau  31259  issh  31283  isch  31297  elcnop  31932  ellnop  31933  elbdop  31935  elhmop  31948  elcnfn  31957  ellnfn  31958  isst  32288  ishst  32289  ela  32414  isslmd  33284  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspn  33328  ssdifidllem  33537  ssdifidlprm  33539  ssmxidllem  33554  isufd  33621  iscref  34001  isrrext  34157  ispisys  34309  isldsys  34313  isros  34325  issros  34332  oddpwdc  34511  eulerpartleme  34520  eulerpartlemo  34522  eulerpartlemd  34523  eulerpartlemt0  34526  eulerpartlemf  34527  eulerpartlemt  34528  eulerpartlemr  34531  eulerpartlemmf  34532  eulerpartlemgvv  34533  eulerpartlemgs2  34537  eulerpartlemn  34538  elprob  34566  ballotlemelo  34645  ballotleme  34654  bnj1152  35154  bnj1280  35176  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem1  35385  ispconn  35417  issconn  35420  cvmsiota  35471  cvmlift2lem12  35508  fmla1  35581  gonan0  35586  goaln0  35587  gonar  35589  goalr  35591  sategoelfvb  35613  rdgprc0  35985  elwlim  36015  neibastop1  36553  neibastop2lem  36554  neibastop2  36555  topdifinffinlem  37552  pibp19  37619  pibp21  37620  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  isprrngo  38251  rabeqel  38452  toycom  39233  isopos  39440  isoml  39498  isatl  39559  iscvlat  39583  ishlat1  39612  cdlemm10N  41378  dihglblem2N  41554  lcfl1lem  41751  lcfls1lem  41794  mapdordlem1a  41894  mapdordlem1  41896  iscsrg  42224  readvcot  42619  mhphflem  42839  pellqrex  43121  islnm  43319  pwssplit4  43331  islnr  43353  fnlimcnv  45911  stoweidlem14  46258  stoweidlem16  46260  stoweidlem37  46281  stoweidlem48  46292  stoweidlem51  46295  stoweidlem59  46303  salexct  46578  salexct2  46583  salexct3  46586  salgencntex  46587  salgensscntex  46588  ovn0lem  46809  opnvonmbllem1  46876  ovolval5lem2  46897  pimincfltioc  46960  pimdecfgtioo  46961  pimincfltioo  46962  smfresal  47032  smfmullem2  47036  smfpimbor1lem1  47042  smfpimbor1lem2  47043  smfinflem  47061  sprsymrelfo  47743  prproropf1olem1  47749  pairreueq  47756  iseven  47874  isodd  47875  m1expevenALTV  47893  iseven2  47897  isodd3  47898  odd2np1ALTV  47920  opoeALTV  47929  opeoALTV  47930  isgbe  47997  isgbow  47998  isgbo  47999  uspgrlimlem2  48235  uspgrlimlem3  48236  uspgrlimlem4  48237  clnbgrvtxedg  48240  grlimpredg  48244  grlimprclnbgrvtx  48245  grlimgrtrilem1  48247  0nodd  48416  1odd  48417  2nodd  48418  iscmgmALT  48470  issgrpALT  48471  iscsgrpALT  48472  1neven  48484  2zlidl  48486  2zrngamgm  48491  2zrngagrp  48495  2zrngmmgm  48498  2zrngnmrid  48502  itsclc0  49017  itsclc0b  49018  isthinc  49664  istermc  49719