Theorem elrab2 3685

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099  {crab 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473

This theorem is referenced by:  rru  3774  elrabsf  3825  fvmpti  7004  fvmptss2  7031  tfis  7859  elom  7873  oawordeulem  8575  oeeulem  8622  mapfienlem1  9429  mapfienlem3  9431  mapfien  9432  ordtypelem2  9543  ordtypelem3  9544  ordtypelem9  9550  wemapso2lem  9576  inf3lema  9648  oemapvali  9708  tz9.12lem3  9813  cofsmo  10293  enfin2i  10345  fin23lem28  10364  isf32lem6  10382  hsmexlem4  10453  zorn2lem2  10521  pwfseqlem1  10682  pwfseqlem3  10684  nqereu  10953  elz  12591  zsupss  12952  rpnnen1lem5  12996  elrp  13009  repos  13456  wwlktovf  14940  wwlktovf1  14941  wwlktovfo  14942  01sqrexlem1  15222  01sqrexlem2  15223  01sqrexlem6  15227  01sqrexlem7  15228  ello1  15492  elo1  15503  rlimrege0  15556  divalglem2  16372  divalglem4  16373  divalglem5  16374  divalglem9  16378  divalglem10  16379  bitsfzolem  16409  gcdcllem1  16474  gcdcllem2  16475  gcdcllem3  16476  bezoutlem1  16515  bezoutlem3  16517  bezoutlem4  16518  isprm  16644  maxprmfct  16680  phimullem  16748  eulerthlem1  16750  eulerthlem2  16751  hashgcdlem  16757  pclem  16807  pcprecl  16808  pcprendvds  16809  infpn2  16882  prmreclem1  16885  prmreclem2  16886  prmreclem3  16887  prmreclem5  16889  1arith  16896  elgz  16900  4sqlem13  16926  4sqlem17  16930  4sqlem18  16931  vdwnnlem2  16965  vdwnnlem3  16966  ramtlecl  16969  isdrs  18293  istos  18410  islat  18425  isclat  18492  isdlat  18514  istsr  18575  issgrp  18680  ismnddef  18696  gsumvallem2  18786  isgrp  18896  elnmz  19118  gastacl  19260  gastacos  19261  symgfixelq  19388  psgneldm  19458  sylow1lem2  19554  sylow1lem4  19556  sylow2alem1  19572  sylow2alem2  19573  efgsdm  19685  iscmn  19744  iscyg  19834  iscyggen  19835  dprdw  19967  ablfacrplem  20022  ablfacrp  20023  ablfac1c  20028  ablfac1eu  20030  pgpfaclem1  20038  ablfaclem3  20044  ablfac2  20046  issimpg  20049  isrng  20094  issrg  20128  isring  20177  iscrng  20180  isnzr  20453  islring  20477  isdrng  20628  islmod  20747  islvec  20989  lspsolvlem  21030  lbsextlem1  21046  lbsextlem3  21048  lbsextlem4  21049  islpir  21218  isrrg  21235  isdomn  21241  isphl  21560  pjdm  21641  ishil  21652  frlmssuvc1  21728  frlmssuvc2  21729  frlmsslsp  21730  isassa  21790  psrbag  21850  psrbaglefi  21865  psrbaglefiOLD  21866  psrbagconcl  21867  psrbagconclOLD  21868  psrbagleadd1  21869  psrbagconf1oOLD  21871  gsumbagdiaglemOLD  21872  gsumbagdiaglem  21875  mplelbas  21933  gsummatr01lem1  22570  gsummatr01lem4  22573  gsummatr01  22574  mretopd  23009  neipeltop  23046  isperf  23068  ist0  23237  ist1  23238  ishaus  23239  iscnrm  23240  isreg  23249  isnrm  23252  ispnrm  23256  iscmp  23305  hauscmplem  23323  isconn  23330  conncompss  23350  is1stc  23358  islly  23385  isnlly  23386  dfac14lem  23534  ishmeo  23676  ptcmplem3  23971  ptcmplem4  23972  istmd  23991  istgp  23994  tgpconncompeqg  24029  tgpt0  24036  qustgpopn  24037  istrg  24081  istdrg  24083  istlm  24102  istvc  24109  iscusp  24217  imasdsf1olem  24292  isxms  24366  isms  24368  blcld  24427  prdsxmslem2  24451  isngp  24518  isnrg  24590  isnlm  24605  icccmplem1  24751  icccmplem2  24752  isclm  25004  iscph  25111  isbn  25279  iscms  25286  ivthlem1  25393  ivthlem2  25394  ivthlem3  25395  elovolm  25417  ovolicc2lem2  25460  ovolicc2lem4  25462  ovolicc2lem5  25463  ismbl  25468  dyadmbllem  25541  dyadmbl  25542  ismbf1  25566  isi1f  25616  isibl  25708  isuc1p  26089  ismon1p  26091  radcnvle  26369  abelthlem2  26382  abelthlem7a  26387  atans  26875  lgamgulmlem2  26975  lgamgulmlem3  26976  lgamgulmlem5  26978  lgambdd  26982  wilthlem2  27014  wilthlem3  27015  ftalem3  27020  sqff1o  27127  mpodvdsmulf1o  27139  dvdsmulf1o  27141  lgslem2  27244  lgslem3  27245  lgsfcl2  27249  rpvmasumlem  27433  dchrvmaeq0  27450  dchrisum0re  27459  pntlem3  27555  0elleft  27849  0elright  27850  addsproplem4  27902  addsproplem5  27903  addsproplem6  27904  negsproplem4  27956  negsproplem5  27957  mulsproplem12  28040  precsexlem8  28125  precsexlem9  28126  precsexlem11  28128  elons  28159  sltonold  28166  elreno  28236  axcontlem2  28789  lfgredgge2  28950  uspgredg2vlem  29049  uspgredg2v  29050  usgredg2vlem1  29051  usgredg2vlem2  29052  ushgredgedg  29055  ushgredgedgloop  29057  uhgrspan1  29129  upgrreslem  29130  umgrreslem  29131  isfusgr  29144  nbupgrres  29190  nbusgredgeu0  29194  nbusgrf1o0  29195  uvtxel  29214  uvtxel1  29222  cusgrexilem2  29268  cusgrfilem2  29283  vtxdginducedm1lem4  29369  rgrx0ndm  29420  iswspthn  29673  wwlknon  29681  wspthnon  29682  wwlksn0  29687  wwlksnextfun  29722  wwlksnextinj  29723  wwlksnextsurj  29724  wwlksnextproplem3  29735  clwlkclwwlkflem  29827  clwlkclwwlkfolem  29830  isclwwlkn  29850  clwwlkel  29869  clwwlkf  29870  clwwlkf1  29872  isclwwlknon  29914  s2elclwwlknon2  29927  isfrgr  30083  frgrwopreglem3  30137  frgrwopreglem5lem  30143  frgrwopreglem5  30144  isablo  30369  iscbn  30687  hcau  31007  issh  31031  isch  31045  elcnop  31680  ellnop  31681  elbdop  31683  elhmop  31696  elcnfn  31705  ellnfn  31706  isst  32036  ishst  32037  ela  32162  isomnd  32794  isslmd  32922  isorng  33027  ssmxidllem  33199  isufd  33242  iscref  33445  isrrext  33601  ispisys  33771  isldsys  33775  isros  33787  issros  33794  oddpwdc  33974  eulerpartleme  33983  eulerpartlemo  33985  eulerpartlemd  33986  eulerpartlemt0  33989  eulerpartlemf  33990  eulerpartlemt  33991  eulerpartlemr  33994  eulerpartlemmf  33995  eulerpartlemgvv  33996  eulerpartlemgs2  34000  eulerpartlemn  34001  elprob  34029  ballotlemelo  34107  ballotleme  34116  bnj1152  34629  bnj1280  34651  subfacp1lem3  34792  subfacp1lem5  34794  erdszelem1  34801  ispconn  34833  issconn  34836  cvmsiota  34887  cvmlift2lem12  34924  fmla1  34997  gonan0  35002  goaln0  35003  gonar  35005  goalr  35007  sategoelfvb  35029  rdgprc0  35389  elwlim  35419  neibastop1  35843  neibastop2lem  35844  neibastop2  35845  topdifinffinlem  36826  pibp19  36893  pibp21  36894  poimirlem5  37098  poimirlem6  37099  poimirlem7  37100  poimirlem8  37101  poimirlem10  37103  poimirlem11  37104  poimirlem12  37105  poimirlem15  37108  poimirlem16  37109  poimirlem17  37110  poimirlem18  37111  poimirlem19  37112  poimirlem20  37113  poimirlem21  37114  poimirlem22  37115  isprrngo  37523  rabeqel  37726  toycom  38445  isopos  38652  isoml  38710  isatl  38771  iscvlat  38795  ishlat1  38824  cdlemm10N  40591  dihglblem2N  40767  lcfl1lem  40964  lcfls1lem  41007  mapdordlem1a  41107  mapdordlem1  41109  iscsrg  41441  mhphflem  41829  pellqrex  42299  islnm  42501  pwssplit4  42513  islnr  42535  fnlimcnv  45055  stoweidlem14  45402  stoweidlem16  45404  stoweidlem37  45425  stoweidlem48  45436  stoweidlem51  45439  stoweidlem59  45447  salexct  45722  salexct2  45727  salexct3  45730  salgencntex  45731  salgensscntex  45732  ovn0lem  45953  opnvonmbllem1  46020  ovolval5lem2  46041  pimincfltioc  46104  pimdecfgtioo  46105  pimincfltioo  46106  smfresal  46176  smfmullem2  46180  smfpimbor1lem1  46186  smfpimbor1lem2  46187  smfinflem  46205  sprsymrelfo  46837  prproropf1olem1  46843  pairreueq  46850  iseven  46968  isodd  46969  m1expevenALTV  46987  iseven2  46991  isodd3  46992  odd2np1ALTV  47014  opoeALTV  47023  opeoALTV  47024  isgbe  47091  isgbow  47092  isgbo  47093  0nodd  47232  1odd  47233  2nodd  47234  iscmgmALT  47286  issgrpALT  47287  iscsgrpALT  47288  1neven  47300  2zlidl  47302  2zrngamgm  47307  2zrngagrp  47311  2zrngmmgm  47314  2zrngnmrid  47318  itsclc0  47844  itsclc0b  47845  isthinc  48027