Theorem elrab2 3697

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479

This theorem is referenced by:  rru  3787  elrabsf  3839  fvmpti  7014  fvmptss2  7041  tfis  7875  elom  7889  oawordeulem  8590  oeeulem  8637  mapfienlem1  9442  mapfienlem3  9444  mapfien  9445  ordtypelem2  9556  ordtypelem3  9557  ordtypelem9  9563  wemapso2lem  9589  inf3lema  9661  oemapvali  9721  tz9.12lem3  9826  cofsmo  10306  enfin2i  10358  fin23lem28  10377  isf32lem6  10395  hsmexlem4  10466  zorn2lem2  10534  pwfseqlem1  10695  pwfseqlem3  10697  nqereu  10966  elz  12612  zsupss  12976  rpnnen1lem5  13020  elrp  13033  repos  13482  wwlktovf  14991  wwlktovf1  14992  wwlktovfo  14993  01sqrexlem1  15277  01sqrexlem2  15278  01sqrexlem6  15282  01sqrexlem7  15283  ello1  15547  elo1  15558  rlimrege0  15611  divalglem2  16428  divalglem4  16429  divalglem5  16430  divalglem9  16434  divalglem10  16435  bitsfzolem  16467  gcdcllem1  16532  gcdcllem2  16533  gcdcllem3  16534  bezoutlem1  16572  bezoutlem3  16574  bezoutlem4  16575  isprm  16706  maxprmfct  16742  phimullem  16812  eulerthlem1  16814  eulerthlem2  16815  hashgcdlem  16821  pclem  16871  pcprecl  16872  pcprendvds  16873  infpn2  16946  prmreclem1  16949  prmreclem2  16950  prmreclem3  16951  prmreclem5  16953  1arith  16960  elgz  16964  4sqlem13  16990  4sqlem17  16994  4sqlem18  16995  vdwnnlem2  17029  vdwnnlem3  17030  ramtlecl  17033  isdrs  18358  istos  18475  islat  18490  isclat  18557  isdlat  18579  istsr  18640  issgrp  18745  ismnddef  18761  gsumvallem2  18859  isgrp  18969  elnmz  19193  gastacl  19339  gastacos  19340  symgfixelq  19465  psgneldm  19535  sylow1lem2  19631  sylow1lem4  19633  sylow2alem1  19649  sylow2alem2  19650  efgsdm  19762  iscmn  19821  iscyg  19911  iscyggen  19912  dprdw  20044  ablfacrplem  20099  ablfacrp  20100  ablfac1c  20105  ablfac1eu  20107  pgpfaclem1  20115  ablfaclem3  20121  ablfac2  20123  issimpg  20126  isrng  20171  issrg  20205  isring  20254  iscrng  20257  isnzr  20530  islring  20556  isrrg  20714  isdomn  20721  isdrng  20749  islmod  20878  islvec  21120  lspsolvlem  21161  lbsextlem1  21177  lbsextlem3  21179  lbsextlem4  21180  islpir  21355  isphl  21663  pjdm  21744  ishil  21755  frlmssuvc1  21831  frlmssuvc2  21832  frlmsslsp  21833  isassa  21893  psrbag  21954  psrbaglefi  21963  psrbagconcl  21964  psrbagleadd1  21965  gsumbagdiaglem  21967  mplelbas  22028  gsummatr01lem1  22676  gsummatr01lem4  22679  gsummatr01  22680  mretopd  23115  neipeltop  23152  isperf  23174  ist0  23343  ist1  23344  ishaus  23345  iscnrm  23346  isreg  23355  isnrm  23358  ispnrm  23362  iscmp  23411  hauscmplem  23429  isconn  23436  conncompss  23456  is1stc  23464  islly  23491  isnlly  23492  dfac14lem  23640  ishmeo  23782  ptcmplem3  24077  ptcmplem4  24078  istmd  24097  istgp  24100  tgpconncompeqg  24135  tgpt0  24142  qustgpopn  24143  istrg  24187  istdrg  24189  istlm  24208  istvc  24215  iscusp  24323  imasdsf1olem  24398  isxms  24472  isms  24474  blcld  24533  prdsxmslem2  24557  isngp  24624  isnrg  24696  isnlm  24711  icccmplem1  24857  icccmplem2  24858  isclm  25110  iscph  25217  isbn  25385  iscms  25392  ivthlem1  25499  ivthlem2  25500  ivthlem3  25501  elovolm  25523  ovolicc2lem2  25566  ovolicc2lem4  25568  ovolicc2lem5  25569  ismbl  25574  dyadmbllem  25647  dyadmbl  25648  ismbf1  25672  isi1f  25722  isibl  25814  isuc1p  26194  ismon1p  26196  radcnvle  26477  abelthlem2  26490  abelthlem7a  26495  atans  26987  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgambdd  27094  wilthlem2  27126  wilthlem3  27127  ftalem3  27132  sqff1o  27239  mpodvdsmulf1o  27251  dvdsmulf1o  27253  lgslem2  27356  lgslem3  27357  lgsfcl2  27361  rpvmasumlem  27545  dchrvmaeq0  27562  dchrisum0re  27571  pntlem3  27667  0elleft  27962  0elright  27963  addsproplem4  28019  addsproplem5  28020  addsproplem6  28021  negsproplem4  28077  negsproplem5  28078  mulsproplem12  28167  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255  elons  28290  sltonold  28297  elreno  28441  axcontlem2  28994  lfgredgge2  29155  uspgredg2vlem  29254  uspgredg2v  29255  usgredg2vlem1  29256  usgredg2vlem2  29257  ushgredgedg  29260  ushgredgedgloop  29262  uhgrspan1  29334  upgrreslem  29335  umgrreslem  29336  isfusgr  29349  nbupgrres  29395  nbusgredgeu0  29399  nbusgrf1o0  29400  uvtxel  29419  uvtxel1  29427  cusgrexilem2  29473  cusgrfilem2  29488  vtxdginducedm1lem4  29574  rgrx0ndm  29625  iswspthn  29878  wwlknon  29886  wspthnon  29887  wwlksn0  29892  wwlksnextfun  29927  wwlksnextinj  29928  wwlksnextsurj  29929  wwlksnextproplem3  29940  clwlkclwwlkflem  30032  clwlkclwwlkfolem  30035  isclwwlkn  30055  clwwlkel  30074  clwwlkf  30075  clwwlkf1  30077  isclwwlknon  30119  s2elclwwlknon2  30132  isfrgr  30288  frgrwopreglem3  30342  frgrwopreglem5lem  30348  frgrwopreglem5  30349  isablo  30574  iscbn  30892  hcau  31212  issh  31236  isch  31250  elcnop  31885  ellnop  31886  elbdop  31888  elhmop  31901  elcnfn  31910  ellnfn  31911  isst  32241  ishst  32242  ela  32367  ischn  32980  isomnd  33060  isslmd  33190  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  isorng  33308  ssdifidllem  33463  ssdifidlprm  33465  ssmxidllem  33480  isufd  33547  iscref  33804  isrrext  33962  ispisys  34132  isldsys  34136  isros  34148  issros  34155  oddpwdc  34335  eulerpartleme  34344  eulerpartlemo  34346  eulerpartlemd  34347  eulerpartlemt0  34350  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgs2  34361  eulerpartlemn  34362  elprob  34390  ballotlemelo  34468  ballotleme  34477  bnj1152  34990  bnj1280  35012  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem1  35175  ispconn  35207  issconn  35210  cvmsiota  35261  cvmlift2lem12  35298  fmla1  35371  gonan0  35376  goaln0  35377  gonar  35379  goalr  35381  sategoelfvb  35403  rdgprc0  35774  elwlim  35804  neibastop1  36341  neibastop2lem  36342  neibastop2  36343  topdifinffinlem  37329  pibp19  37396  pibp21  37397  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  isprrngo  38036  rabeqel  38235  toycom  38954  isopos  39161  isoml  39219  isatl  39280  iscvlat  39304  ishlat1  39333  cdlemm10N  41100  dihglblem2N  41276  lcfl1lem  41473  lcfls1lem  41516  mapdordlem1a  41616  mapdordlem1  41618  iscsrg  41950  mhphflem  42582  pellqrex  42866  islnm  43065  pwssplit4  43077  islnr  43099  fnlimcnv  45622  stoweidlem14  45969  stoweidlem16  45971  stoweidlem37  45992  stoweidlem48  46003  stoweidlem51  46006  stoweidlem59  46014  salexct  46289  salexct2  46294  salexct3  46297  salgencntex  46298  salgensscntex  46299  ovn0lem  46520  opnvonmbllem1  46587  ovolval5lem2  46608  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  smfresal  46743  smfmullem2  46747  smfpimbor1lem1  46753  smfpimbor1lem2  46754  smfinflem  46772  sprsymrelfo  47421  prproropf1olem1  47427  pairreueq  47434  iseven  47552  isodd  47553  m1expevenALTV  47571  iseven2  47575  isodd3  47576  odd2np1ALTV  47598  opoeALTV  47607  opeoALTV  47608  isgbe  47675  isgbow  47676  isgbo  47677  uspgrlimlem2  47891  uspgrlimlem3  47892  uspgrlimlem4  47893  0nodd  48013  1odd  48014  2nodd  48015  iscmgmALT  48067  issgrpALT  48068  iscsgrpALT  48069  1neven  48081  2zlidl  48083  2zrngamgm  48088  2zrngagrp  48092  2zrngmmgm  48095  2zrngnmrid  48099  itsclc0  48620  itsclc0b  48621  isthinc  48820