Theorem elrab2 3651

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448

This theorem is referenced by:  rru  3740  elrabsf  3790  fvmpti  6952  fvmptss2  6978  tfis  7796  elom  7810  oawordeulem  8506  oeeulem  8553  mapfienlem1  9350  mapfienlem3  9352  mapfien  9353  ordtypelem2  9464  ordtypelem3  9465  ordtypelem9  9471  wemapso2lem  9497  inf3lema  9569  oemapvali  9629  tz9.12lem3  9734  cofsmo  10214  enfin2i  10266  fin23lem28  10285  isf32lem6  10303  hsmexlem4  10374  zorn2lem2  10442  pwfseqlem1  10603  pwfseqlem3  10605  nqereu  10874  elz  12510  zsupss  12871  rpnnen1lem5  12915  elrp  12926  repos  13373  wwlktovf  14857  wwlktovf1  14858  wwlktovfo  14859  01sqrexlem1  15139  01sqrexlem2  15140  01sqrexlem6  15144  01sqrexlem7  15145  ello1  15409  elo1  15420  rlimrege0  15473  divalglem2  16288  divalglem4  16289  divalglem5  16290  divalglem9  16294  divalglem10  16295  bitsfzolem  16325  gcdcllem1  16390  gcdcllem2  16391  gcdcllem3  16392  bezoutlem1  16431  bezoutlem3  16433  bezoutlem4  16434  isprm  16560  maxprmfct  16596  phimullem  16662  eulerthlem1  16664  eulerthlem2  16665  hashgcdlem  16671  pclem  16721  pcprecl  16722  pcprendvds  16723  infpn2  16796  prmreclem1  16799  prmreclem2  16800  prmreclem3  16801  prmreclem5  16803  1arith  16810  elgz  16814  4sqlem13  16840  4sqlem17  16844  4sqlem18  16845  vdwnnlem2  16879  vdwnnlem3  16880  ramtlecl  16883  isdrs  18204  istos  18321  islat  18336  isclat  18403  isdlat  18425  istsr  18486  issgrp  18561  ismnddef  18572  gsumvallem2  18658  isgrp  18768  elnmz  18979  gastacl  19103  gastacos  19104  symgfixelq  19229  psgneldm  19299  sylow1lem2  19395  sylow1lem4  19397  sylow2alem1  19413  sylow2alem2  19414  efgsdm  19526  iscmn  19585  iscyg  19670  iscyggen  19671  dprdw  19803  ablfacrplem  19858  ablfacrp  19859  ablfac1c  19864  ablfac1eu  19866  pgpfaclem1  19874  ablfaclem3  19880  ablfac2  19882  issimpg  19885  issrg  19933  isring  19982  iscrng  19985  isnzr  20203  islring  20220  isdrng  20229  islmod  20382  islvec  20622  lspsolvlem  20662  lbsextlem1  20678  lbsextlem3  20680  lbsextlem4  20681  islpir  20778  isrrg  20795  isdomn  20801  isphl  21069  pjdm  21150  ishil  21161  frlmssuvc1  21237  frlmssuvc2  21238  frlmsslsp  21239  isassa  21299  psrbag  21356  psrbaglefi  21371  psrbaglefiOLD  21372  psrbagconcl  21373  psrbagconclOLD  21374  psrbagconf1oOLD  21376  gsumbagdiaglemOLD  21377  gsumbagdiaglem  21380  mplelbas  21436  gsummatr01lem1  22041  gsummatr01lem4  22044  gsummatr01  22045  mretopd  22480  neipeltop  22517  isperf  22539  ist0  22708  ist1  22709  ishaus  22710  iscnrm  22711  isreg  22720  isnrm  22723  ispnrm  22727  iscmp  22776  hauscmplem  22794  isconn  22801  conncompss  22821  is1stc  22829  islly  22856  isnlly  22857  dfac14lem  23005  ishmeo  23147  ptcmplem3  23442  ptcmplem4  23443  istmd  23462  istgp  23465  tgpconncompeqg  23500  tgpt0  23507  qustgpopn  23508  istrg  23552  istdrg  23554  istlm  23573  istvc  23580  iscusp  23688  imasdsf1olem  23763  isxms  23837  isms  23839  blcld  23898  prdsxmslem2  23922  isngp  23989  isnrg  24061  isnlm  24076  icccmplem1  24222  icccmplem2  24223  isclm  24464  iscph  24571  isbn  24739  iscms  24746  ivthlem1  24852  ivthlem2  24853  ivthlem3  24854  elovolm  24876  ovolicc2lem2  24919  ovolicc2lem4  24921  ovolicc2lem5  24922  ismbl  24927  dyadmbllem  25000  dyadmbl  25001  ismbf1  25025  isi1f  25075  isibl  25167  isuc1p  25542  ismon1p  25544  radcnvle  25816  abelthlem2  25828  abelthlem7a  25833  atans  26317  lgamgulmlem2  26416  lgamgulmlem3  26417  lgamgulmlem5  26419  lgambdd  26423  wilthlem2  26455  wilthlem3  26456  ftalem3  26461  sqff1o  26568  dvdsmulf1o  26580  lgslem2  26683  lgslem3  26684  lgsfcl2  26688  rpvmasumlem  26872  dchrvmaeq0  26889  dchrisum0re  26898  pntlem3  26994  addsproplem4  27327  addsproplem5  27328  addsproplem6  27329  negsproplem4  27372  negsproplem5  27373  axcontlem2  27977  lfgredgge2  28138  uspgredg2vlem  28234  uspgredg2v  28235  usgredg2vlem1  28236  usgredg2vlem2  28237  ushgredgedg  28240  ushgredgedgloop  28242  uhgrspan1  28314  upgrreslem  28315  umgrreslem  28316  isfusgr  28329  nbupgrres  28375  nbusgredgeu0  28379  nbusgrf1o0  28380  uvtxel  28399  uvtxel1  28407  cusgrexilem2  28453  cusgrfilem2  28467  vtxdginducedm1lem4  28553  rgrx0ndm  28604  iswspthn  28857  wwlknon  28865  wspthnon  28866  wwlksn0  28871  wwlksnextfun  28906  wwlksnextinj  28907  wwlksnextsurj  28908  wwlksnextproplem3  28919  clwlkclwwlkflem  29011  clwlkclwwlkfolem  29014  isclwwlkn  29034  clwwlkel  29053  clwwlkf  29054  clwwlkf1  29056  isclwwlknon  29098  s2elclwwlknon2  29111  isfrgr  29267  frgrwopreglem3  29321  frgrwopreglem5lem  29327  frgrwopreglem5  29328  isablo  29551  iscbn  29869  hcau  30189  issh  30213  isch  30227  elcnop  30862  ellnop  30863  elbdop  30865  elhmop  30878  elcnfn  30887  ellnfn  30888  isst  31218  ishst  31219  ela  31344  isomnd  31979  isslmd  32107  isorng  32165  ssmxidllem  32314  isufd  32336  iscref  32514  isrrext  32670  ispisys  32840  isldsys  32844  isros  32856  issros  32863  oddpwdc  33043  eulerpartleme  33052  eulerpartlemo  33054  eulerpartlemd  33055  eulerpartlemt0  33058  eulerpartlemf  33059  eulerpartlemt  33060  eulerpartlemr  33063  eulerpartlemmf  33064  eulerpartlemgvv  33065  eulerpartlemgs2  33069  eulerpartlemn  33070  elprob  33098  ballotlemelo  33176  ballotleme  33185  bnj1152  33699  bnj1280  33721  subfacp1lem3  33863  subfacp1lem5  33865  erdszelem1  33872  ispconn  33904  issconn  33907  cvmsiota  33958  cvmlift2lem12  33995  fmla1  34068  gonan0  34073  goaln0  34074  gonar  34076  goalr  34078  sategoelfvb  34100  rdgprc0  34454  elwlim  34484  neibastop1  34907  neibastop2lem  34908  neibastop2  34909  topdifinffinlem  35891  pibp19  35958  pibp21  35959  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem8  36159  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem15  36166  poimirlem16  36167  poimirlem17  36168  poimirlem18  36169  poimirlem19  36170  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  isprrngo  36582  rabeqel  36787  toycom  37508  isopos  37715  isoml  37773  isatl  37834  iscvlat  37858  ishlat1  37887  cdlemm10N  39654  dihglblem2N  39830  lcfl1lem  40027  lcfls1lem  40070  mapdordlem1a  40170  mapdordlem1  40172  mhphflem  40828  pellqrex  41260  islnm  41462  pwssplit4  41474  islnr  41496  fnlimcnv  44028  stoweidlem14  44375  stoweidlem16  44377  stoweidlem37  44398  stoweidlem48  44409  stoweidlem51  44412  stoweidlem59  44420  salexct  44695  salexct2  44700  salexct3  44703  salgencntex  44704  salgensscntex  44705  ovn0lem  44926  opnvonmbllem1  44993  ovolval5lem2  45014  pimincfltioc  45077  pimdecfgtioo  45078  pimincfltioo  45079  smfresal  45149  smfmullem2  45153  smfpimbor1lem1  45159  smfpimbor1lem2  45160  smfinflem  45178  sprsymrelfo  45809  prproropf1olem1  45815  pairreueq  45822  iseven  45940  isodd  45941  m1expevenALTV  45959  iseven2  45963  isodd3  45964  odd2np1ALTV  45986  opoeALTV  45995  opeoALTV  45996  isgbe  46063  isgbow  46064  isgbo  46065  0nodd  46224  1odd  46225  2nodd  46226  iscmgmALT  46278  issgrpALT  46279  iscsgrpALT  46280  isrng  46294  1neven  46350  2zlidl  46352  2zrngamgm  46357  2zrngagrp  46361  2zrngmmgm  46364  2zrngnmrid  46368  itsclc0  46977  itsclc0b  46978  isthinc  47161