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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453

This theorem is used by:  rru  3737  elrabsf  3784  fvmpti  6990  fvmptss2  7018  tfis  7864  elom  7878  oawordeulem  8555  oeeulem  8603  mapfienlem1  9390  mapfienlem3  9392  mapfien  9393  ordtypelem2  9506  ordtypelem3  9507  ordtypelem9  9513  wemapso2lem  9539  inf3lema  9618  oemapvali  9678  tz9.12lem3  9789  cofsmo  10340  enfin2i  10392  fin23lem28  10411  isf32lem6  10429  hsmexlem4  10500  zorn2lem2  10568  pwfseqlem1  10736  pwfseqlem3  10738  nqereu  11007  elz  12688  zsupss  13057  rpnnen1lem5  13102  elrp  13115  repos  13570  wwlktovf  15102  wwlktovf1  15103  wwlktovfo  15104  01sqrexlem1  15402  01sqrexlem2  15403  01sqrexlem6  15407  01sqrexlem7  15408  ello1  15675  elo1  15686  rlimrege0  15739  divalglem2  16558  divalglem4  16559  divalglem5  16560  divalglem9  16564  divalglem10  16565  bitsfzolem  16597  gcdcllem1  16662  gcdcllem2  16663  gcdcllem3  16664  bezoutlem1  16705  bezoutlem3  16707  bezoutlem4  16708  isprm  16841  maxprmfct  16878  phimullem  16949  eulerthlem1  16951  eulerthlem2  16952  hashgcdlem  16958  pclem  17009  pcprecl  17010  pcprendvds  17011  infpn2  17084  prmreclem1  17087  prmreclem2  17088  prmreclem3  17089  prmreclem5  17091  1arith  17098  elgz  17102  4sqlem13  17128  4sqlem17  17132  4sqlem18  17133  vdwnnlem2  17167  vdwnnlem3  17168  ramtlecl  17171  isdrs  18468  istos  18583  islat  18600  isclat  18667  isdlat  18689  istsr  18750  ischn  18774  issgrp  18902  ismnddef  18918  gsumvallem2  19023  isgrp  19143  elnmz  19366  gastacl  19516  gastacos  19517  symgfixelq  19640  psgneldm  19710  sylow1lem2  19806  sylow1lem4  19808  sylow2alem1  19824  sylow2alem2  19825  efgsdm  19937  iscmn  19996  iscyg  20086  iscyggen  20087  dprdw  20219  ablfacrplem  20274  ablfacrp  20275  ablfac1c  20280  ablfac1eu  20282  pgpfaclem1  20290  ablfaclem3  20296  ablfac2  20298  issimpg  20301  isomnd  20330  isrng  20369  issrg  20407  isring  20456  iscrng  20459  isnzr  20757  islring  20785  isrrg  20943  isdomn  20950  isdrng  20977  isorng  21111  islmod  21132  islvec  21372  lspsolvlem  21413  lbsextlem1  21429  lbsextlem3  21431  lbsextlem4  21432  ssdifidllem  21633  ssdifidlprm  21635  islpir  21645  isphl  21927  pjdm  22006  ishil  22017  frlmssuvc1  22093  frlmssuvc2  22094  frlmsslsp  22095  isassa  22157  psrbag  22218  psrbaglefi  22227  psrbagconcl  22228  psrbagleadd1  22229  gsumbagdiaglem  22232  mplelbas  22291  gsummatr01lem1  22963  gsummatr01lem4  22966  gsummatr01  22967  mretopd  23403  neipeltop  23440  isperf  23462  ist0  23631  ist1  23632  ishaus  23633  iscnrm  23634  isreg  23643  isnrm  23646  ispnrm  23650  iscmp  23699  hauscmplem  23717  isconn  23724  conncompss  23744  is1stc  23752  islly  23780  isnlly  23781  dfac14lem  23929  ishmeo  24071  ptcmplem3  24366  ptcmplem4  24367  istmd  24386  istgp  24389  tgpconncompeqg  24424  tgpt0  24431  qustgpopn  24432  istrg  24476  istdrg  24478  istlm  24497  istvc  24504  iscusp  24610  imasdsf1olem  24685  isxms  24759  isms  24761  blcld  24817  prdsxmslem2  24841  isngp  24908  isnrg  24972  isnlm  24987  icccmplem1  25135  icccmplem2  25136  isclm  25378  iscph  25484  isbn  25652  iscms  25659  ivthlem1  25765  ivthlem2  25766  ivthlem3  25767  elovolm  25789  ovolicc2lem2  25832  ovolicc2lem4  25834  ovolicc2lem5  25835  ismbl  25840  dyadmbllem  25913  dyadmbl  25914  ismbf1  25938  isi1f  25988  isibl  26079  isuc1p  26452  ismon1p  26454  radcnvle  26740  abelthlem2  26752  abelthlem7a  26757  atans  27251  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem5  27353  lgambdd  27357  wilthlem2  27389  wilthlem3  27390  ftalem3  27395  sqff1o  27502  mpodvdsmulf1o  27514  dvdsmulf1o  27516  lgslem2  27618  lgslem3  27619  lgsfcl2  27623  rpvmasumlem  27807  dchrvmaeq0  27824  dchrisum0re  27833  pntlem3  27929  elleft  28230  elright  28231  elons  28632  elreno  28870  axcontlem2  29536  lfgredgge2  29695  uspgredg2vlem  29797  uspgredg2v  29798  usgredg2vlem1  29799  usgredg2vlem2  29800  ushgredgedg  29803  ushgredgedgloop  29805  uhgrspan1  29877  upgrreslem  29878  umgrreslem  29879  isfusgr  29892  nbupgrres  29938  nbusgredgeu0  29942  nbusgrf1o0  29943  uvtxel  29962  uvtxel1  29970  cusgrexilem2  30016  cusgrfilem2  30030  vtxdginducedm1lem4  30116  rgrx0ndm  30167  iswspthn  30431  wwlknon  30439  wspthnon  30440  wwlksn0  30445  wwlksnextfun  30480  wwlksnextinj  30481  wwlksnextsurj  30482  wwlksnextproplem3  30493  clwlkclwwlkflem  30588  clwlkclwwlkfolem  30591  isclwwlkn  30611  clwwlkel  30630  clwwlkf  30631  clwwlkf1  30633  isclwwlknon  30675  s2elclwwlknon2  30688  isfrgr  30854  frgrwopreglem3  30908  frgrwopreglem5lem  30914  frgrwopreglem5  30915  isablo  31141  iscbn  31459  hcau  31779  issh  31803  isch  31817  elcnop  32452  ellnop  32453  elbdop  32455  elhmop  32468  elcnfn  32477  ellnfn  32478  isst  32808  ishst  32809  ela  32934  isslmd  33756  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem4  33799  elrgspn  33800  ssmxidllem  33991  isufd  34065  iscref  34469  isrrext  34625  ispisys  34778  isldsys  34782  isros  34794  issros  34801  oddpwdc  34979  eulerpartleme  34988  eulerpartlemo  34990  eulerpartlemd  34991  eulerpartlemt0  34994  eulerpartlemf  34995  eulerpartlemt  34996  eulerpartlemr  34999  eulerpartlemmf  35000  eulerpartlemgvv  35001  eulerpartlemgs2  35005  eulerpartlemn  35006  elprob  35034  ballotlemelo  35113  ballotleme  35122  bnj1152  35621  bnj1280  35643  elscott  35729  elscott2  35732  elscottrank  35733  subfacp1lem3  35926  subfacp1lem5  35928  erdszelem1  35935  ispconn  35967  issconn  35970  cvmsiota  36021  cvmlift2lem12  36058  fmla1  36131  gonan0  36136  goaln0  36137  gonar  36139  goalr  36141  sategoelfvb  36163  rdgprc0  36535  elwlim  36565  neibastop1  37127  neibastop2lem  37128  neibastop2  37129  topdifinffinlem  38250  pibp19  38317  pibp21  38318  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  isprrngo  38964  rabeqel  39169  toycom  40010  isopos  40217  isoml  40275  isatl  40336  iscvlat  40360  ishlat1  40389  cdlemm10N  42155  dihglblem2N  42331  lcfl1lem  42528  lcfls1lem  42571  mapdordlem1a  42671  mapdordlem1  42673  iscsrg  43001  readvcot  43395  mhphflem  43604  pellqrex  43865  islnm  44063  pwssplit4  44075  islnr  44097  fnlimcnv  46646  stoweidlem14  46993  stoweidlem16  46995  stoweidlem37  47016  stoweidlem48  47027  stoweidlem51  47030  stoweidlem59  47038  salexct  47313  salexct2  47318  salexct3  47321  salgencntex  47322  salgensscntex  47323  ovn0lem  47544  opnvonmbllem1  47611  ovolval5lem2  47632  pimincfltioc  47695  pimdecfgtioo  47696  pimincfltioo  47697  smfresal  47767  smfmullem2  47771  smfpimbor1lem1  47777  smfpimbor1lem2  47778  smfinflem  47796  sprsymrelfo  48548  prproropf1olem1  48554  pairreueq  48561  iseven  48695  isodd  48696  m1expevenALTV  48714  iseven2  48718  isodd3  48719  odd2np1ALTV  48741  opoeALTV  48750  opeoALTV  48751  isgbe  48818  isgbow  48819  isgbo  48820  uspgrlimlem2  49056  uspgrlimlem3  49057  uspgrlimlem4  49058  clnbgrvtxedg  49061  grlimpredg  49065  grlimprclnbgrvtx  49066  grlimgrtrilem1  49068  0nodd  49236  1odd  49237  2nodd  49238  iscmgmALT  49290  issgrpALT  49291  iscsgrpALT  49292  1neven  49304  2zlidl  49306  2zrngamgm  49311  2zrngagrp  49315  2zrngmmgm  49318  2zrngnmrid  49322  isprmrng  49402  itsclc0  49852  itsclc0b  49853  isthinc  50496  istermc  50551