Theorem elrab2 3652

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456

This theorem is used by:  rur  3740  elrabsf  3787  fvmpti  7023  fvmptss2  7051  tfis  7900  elom  7914  oawordeulem  8600  oeeulem  8648  mapfienlem1  9434  mapfienlem3  9436  mapfien  9437  ordtypelem2  9550  ordtypelem3  9551  ordtypelem9  9557  wemapso2lem  9583  inf3lema  9662  oemapvali  9722  tz9.12lem3  9833  cardprcr  10099  cofsmo  10386  enfin2i  10438  fin23lem28  10457  isf32lem6  10475  hsmexlem4  10546  zorn2lem2  10614  pwfseqlem1  10782  pwfseqlem3  10784  nqereu  11053  elz  12735  zsupss  13104  rpnnen1lem5  13149  elrp  13162  repos  13617  wwlktovf  15152  wwlktovf1  15153  wwlktovfo  15154  01sqrexlem1  15452  01sqrexlem2  15453  01sqrexlem6  15457  01sqrexlem7  15458  ello1  15726  elo1  15737  rlimrege0  15790  divalglem2  16609  divalglem4  16610  divalglem5  16611  divalglem9  16615  divalglem10  16616  bitsfzolem  16648  gcdcllem1  16713  gcdcllem2  16714  gcdcllem3  16715  bezoutlem1  16756  bezoutlem3  16758  bezoutlem4  16759  isprm  16892  maxprmfct  16929  phimullem  17000  eulerthlem1  17002  eulerthlem2  17003  hashgcdlem  17009  pclem  17060  pcprecl  17061  pcprendvds  17062  infpn2  17135  prmreclem1  17138  prmreclem2  17139  prmreclem3  17140  prmreclem5  17142  1arith  17149  elgz  17153  4sqlem13  17179  4sqlem17  17183  4sqlem18  17184  vdwnnlem2  17218  vdwnnlem3  17219  ramtlecl  17222  isdrs  18525  istos  18640  islat  18657  isclat  18724  isdlat  18746  istsr  18807  ischn  18831  issgrp  18959  ismnddef  18975  gsumvallem2  19080  isgrp  19200  elnmz  19423  gastacl  19574  gastacos  19575  symgfixelq  19698  psgneldm  19768  sylow1lem2  19864  sylow1lem4  19866  sylow2alem1  19882  sylow2alem2  19883  efgsdm  19995  iscmn  20054  iscyg  20144  iscyggen  20145  dprdw  20277  ablfacrplem  20332  ablfacrp  20333  ablfac1c  20338  ablfac1eu  20340  pgpfaclem1  20348  ablfaclem3  20354  ablfac2  20356  issimpg  20359  isomnd  20388  isrng  20427  issrg  20465  isring  20514  iscrng  20517  isnzr  20815  islring  20843  isrrg  21001  isdomn  21008  isdrng  21035  isorng  21169  islmod  21190  islvec  21430  lspsolvlem  21471  lbsextlem1  21487  lbsextlem3  21489  lbsextlem4  21490  ssdifidllem  21691  ssdifidlprm  21693  islpir  21703  isphl  21989  pjdm  22068  ishil  22079  frlmssuvc1  22155  frlmssuvc2  22156  frlmsslsp  22157  isassa  22219  psrbag  22280  psrbaglefi  22289  psrbagconcl  22290  psrbagleadd1  22291  gsumbagdiaglem  22294  mplelbas  22353  gsummatr01lem1  23025  gsummatr01lem4  23028  gsummatr01  23029  mretopd  23465  neipeltop  23502  isperf  23524  ist0  23693  ist1  23694  ishaus  23695  iscnrm  23696  isreg  23705  isnrm  23708  ispnrm  23712  iscmp  23761  hauscmplem  23779  isconn  23786  conncompss  23806  is1stc  23814  islly  23842  isnlly  23843  dfac14lem  23991  ishmeo  24133  ptcmplem3  24428  ptcmplem4  24429  istmd  24448  istgp  24451  tgpconncompeqg  24486  tgpt0  24493  qustgpopn  24494  istrg  24538  istdrg  24540  istlm  24559  istvc  24566  iscusp  24672  imasdsf1olem  24747  isxms  24821  isms  24823  blcld  24879  prdsxmslem2  24903  isngp  24970  isnrg  25034  isnlm  25049  icccmplem1  25197  icccmplem2  25198  isclm  25440  iscph  25546  isbn  25714  iscms  25721  ivthlem1  25827  ivthlem2  25828  ivthlem3  25829  elovolm  25851  ovolicc2lem2  25894  ovolicc2lem4  25896  ovolicc2lem5  25897  ismbl  25902  dyadmbllem  25975  dyadmbl  25976  ismbf1  26000  isi1f  26050  isibl  26141  isuc1p  26514  ismon1p  26516  radcnvle  26804  abelthlem2  26816  abelthlem7a  26821  atans  27315  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem5  27417  lgambdd  27421  wilthlem2  27453  wilthlem3  27454  ftalem3  27459  sqff1o  27566  mpodvdsmulf1o  27578  dvdsmulf1o  27580  lgslem2  27682  lgslem3  27683  lgsfcl2  27687  rpvmasumlem  27871  dchrvmaeq0  27888  dchrisum0re  27897  pntlem3  27993  elleft  28294  elright  28295  elons  28696  elreno  28934  axcontlem2  29600  lfgredgge2  29759  uspgredg2vlem  29861  uspgredg2v  29862  usgredg2vlem1  29863  usgredg2vlem2  29864  ushgredgedg  29867  ushgredgedgloop  29869  uhgrspan1  29941  upgrreslem  29942  umgrreslem  29943  isfusgr  29956  nbupgrres  30002  nbusgredgeu0  30006  nbusgrf1o0  30007  uvtxel  30026  uvtxel1  30034  cusgrexilem2  30080  cusgrfilem2  30094  vtxdginducedm1lem4  30180  rgrx0ndm  30231  iswspthn  30495  wwlknon  30503  wspthnon  30504  wwlksn0  30509  wwlksnextfun  30544  wwlksnextinj  30545  wwlksnextsurj  30546  wwlksnextproplem3  30557  clwlkclwwlkflem  30652  clwlkclwwlkfolem  30655  isclwwlkn  30675  clwwlkel  30694  clwwlkf  30695  clwwlkf1  30697  isclwwlknon  30739  s2elclwwlknon2  30752  isfrgr  30918  frgrwopreglem3  30972  frgrwopreglem5lem  30978  frgrwopreglem5  30979  isablo  31205  iscbn  31523  hcau  31843  issh  31867  isch  31881  elcnop  32516  ellnop  32517  elbdop  32519  elhmop  32532  elcnfn  32541  ellnfn  32542  isst  32872  ishst  32873  ela  32998  isslmd  33862  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem4  33905  elrgspn  33906  isedom  33953  ssmxidllem  34102  isufd  34176  iscref  34587  isrrext  34743  ispisys  34896  isldsys  34900  isros  34912  issros  34919  oddpwdc  35097  eulerpartleme  35106  eulerpartlemo  35108  eulerpartlemd  35109  eulerpartlemt0  35112  eulerpartlemf  35113  eulerpartlemt  35114  eulerpartlemr  35117  eulerpartlemmf  35118  eulerpartlemgvv  35119  eulerpartlemgs2  35123  eulerpartlemn  35124  elprob  35152  ballotlemelo  35231  ballotleme  35240  bnj1152  35739  bnj1280  35761  elscott  35866  elscott2  35869  elscottrank  35870  subfacp1lem3  36155  subfacp1lem5  36157  erdszelem1  36164  ispconn  36196  issconn  36199  cvmsiota  36250  cvmlift2lem12  36287  fmla1  36360  gonan0  36365  goaln0  36366  gonar  36368  goalr  36370  sategoelfvb  36392  mirimanoffr  36668  mirimanofffr  36670  rdgprc0  36770  elwlim  36800  neibastop1  37362  neibastop2lem  37363  neibastop2  37364  topdifinffinlem  38538  pibp19  38605  pibp21  38606  poimirlem5  38811  poimirlem6  38812  poimirlem7  38813  poimirlem8  38814  poimirlem10  38816  poimirlem11  38817  poimirlem12  38818  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem18  38824  poimirlem19  38825  poimirlem20  38826  poimirlem21  38827  poimirlem22  38828  isprrngo  39250  rabeqel  39455  toycom  40296  isopos  40503  isoml  40561  isatl  40622  iscvlat  40646  ishlat1  40675  cdlemm10N  42441  dihglblem2N  42617  lcfl1lem  42814  lcfls1lem  42857  mapdordlem1a  42957  mapdordlem1  42959  iscsrg  43287  readvcot  43681  mhphflem  43890  pellqrex  44152  islnm  44345  pwssplit4  44357  islnr  44378  fnlimcnv  46950  stoweidlem14  47297  stoweidlem16  47299  stoweidlem37  47320  stoweidlem48  47331  stoweidlem51  47334  stoweidlem59  47342  salexct  47617  salexct2  47622  salexct3  47625  salgencntex  47626  salgensscntex  47627  ovn0lem  47848  opnvonmbllem1  47915  ovolval5lem2  47936  pimincfltioc  47999  pimdecfgtioo  48000  pimincfltioo  48001  smfresal  48071  smfmullem2  48075  smfpimbor1lem1  48081  smfpimbor1lem2  48082  smfinflem  48100  sprsymrelfo  48852  prproropf1olem1  48858  pairreueq  48865  iseven  48999  isodd  49000  m1expevenALTV  49018  iseven2  49022  isodd3  49023  odd2np1ALTV  49045  opoeALTV  49054  opeoALTV  49055  isgbe  49122  isgbow  49123  isgbo  49124  uspgrlimlem2  49360  uspgrlimlem3  49361  uspgrlimlem4  49362  clnbgrvtxedg  49365  grlimpredg  49369  grlimprclnbgrvtx  49370  grlimgrtrilem1  49372  0nodd  49540  1odd  49541  2nodd  49542  iscmgmALT  49594  issgrpALT  49595  iscsgrpALT  49596  1neven  49608  2zlidl  49610  2zrngamgm  49615  2zrngagrp  49619  2zrngmmgm  49622  2zrngnmrid  49626  ellaz  49726  isprmrng  49764  itsclc0  50214  itsclc0b  50215  isthinc  50885  istermc  50940