Theorem elrab2 3366

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)

Hypotheses

Ref	Expression
elrab2.1	|- ( x = A -> ( ph <-> ps ) )
elrab2.2	|- C = { x e. B | ph }

Assertion

Ref	Expression
elrab2	|- ( A e. C <-> ( A e. B /\ ps ) )

Distinct variable groups:   ps, x   x, A   x, B

Allowed substitution hints:   ph( x)   C( x)

Proof of Theorem elrab2

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 |- C = { x e. B | ph }
2	1	eleq2i 2693	. 2 |- ( A e. C <-> A e. { x e. B | ph } )
3		elrab2.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
4	3	elrab 3363	. 2 |- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
5	2, 4	bitri 264	1 |- ( A e. C <-> ( A e. B /\ ps ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202

This theorem is referenced by:  elrabsf  3474  pwnss  4830  fvmpti  6281  fvmptss2  6304  tfis  7054  elom  7068  oawordeulem  7634  oeeulem  7681  mapfienlem1  8310  mapfienlem3  8312  mapfien  8313  ordtypelem2  8424  ordtypelem3  8425  ordtypelem9  8431  wemapso2lem  8457  inf3lema  8521  oemapvali  8581  tz9.12lem3  8652  cofsmo  9091  enfin2i  9143  fin23lem28  9162  isf32lem6  9180  hsmexlem4  9251  zorn2lem2  9319  pwfseqlem1  9480  pwfseqlem3  9482  nqereu  9751  elz  11379  zsupss  11777  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  elrp  11834  repos  12270  wwlktovf  13699  wwlktovf1  13700  wwlktovfo  13701  sqrlem1  13983  sqrlem2  13984  sqrlem6  13988  sqrlem7  13989  ello1  14246  elo1  14257  rlimrege0  14310  divalglem2  15118  divalglem4  15119  divalglem5  15120  divalglem9  15124  divalglem10  15125  bitsfzolem  15156  gcdcllem1  15221  gcdcllem2  15222  gcdcllem3  15223  bezoutlem1  15256  bezoutlem3  15258  bezoutlem4  15259  isprm  15387  maxprmfct  15421  phimullem  15484  eulerthlem1  15486  eulerthlem2  15487  hashgcdlem  15493  pclem  15543  pcprecl  15544  pcprendvds  15545  infpn2  15617  prmreclem1  15620  prmreclem2  15621  prmreclem3  15622  prmreclem5  15624  1arith  15631  elgz  15635  4sqlem13  15661  4sqlem17  15665  4sqlem18  15666  vdwnnlem2  15700  vdwnnlem3  15701  ramtlecl  15704  isdrs  16934  istos  17035  islat  17047  isclat  17109  isdlat  17193  istsr  17217  issgrp  17285  ismnddef  17296  gsumvallem2  17372  isgrp  17428  elnmz  17633  gastacl  17742  gastacos  17743  symgfixelq  17853  psgneldm  17923  sylow1lem2  18014  sylow1lem4  18016  sylow2alem1  18032  sylow2alem2  18033  efgsdm  18143  iscmn  18200  iscyg  18281  iscyggen  18282  dprdw  18409  ablfacrplem  18464  ablfacrp  18465  ablfac1c  18470  ablfac1eu  18472  pgpfaclem1  18480  ablfaclem3  18486  ablfac2  18488  issrg  18507  isring  18551  iscrng  18554  isdrng  18751  islmod  18867  islvec  19104  lspsolvlem  19142  lbsextlem1  19158  lbsextlem3  19160  lbsextlem4  19161  islpir  19249  isnzr  19259  isrrg  19288  isdomn  19294  isassa  19315  psrbag  19364  psrbaglefi  19372  psrbagconcl  19373  psrbagconf1o  19374  gsumbagdiaglem  19375  mplelbas  19430  isphl  19973  pjdm  20051  ishil  20062  frlmssuvc1  20133  frlmssuvc2  20134  frlmsslsp  20135  gsummatr01lem1  20461  gsummatr01lem4  20464  gsummatr01  20465  mretopd  20896  neipeltop  20933  isperf  20955  ist0  21124  ist1  21125  ishaus  21126  iscnrm  21127  isreg  21136  isnrm  21139  ispnrm  21143  iscmp  21191  hauscmplem  21209  isconn  21216  conncompss  21236  is1stc  21244  islly  21271  isnlly  21272  dfac14lem  21420  ishmeo  21562  ptcmplem3  21858  ptcmplem4  21859  istmd  21878  istgp  21881  tgpconncompeqg  21915  tgpt0  21922  qustgpopn  21923  istrg  21967  istdrg  21969  istlm  21988  istvc  21995  iscusp  22103  imasdsf1olem  22178  isxms  22252  isms  22254  blcld  22310  prdsxmslem2  22334  isngp  22400  isnrg  22464  isnlm  22479  icccmplem1  22625  icccmplem2  22626  isclm  22864  iscph  22970  isbn  23135  iscms  23142  ivthlem1  23220  ivthlem2  23221  ivthlem3  23222  elovolm  23243  ovolicc2lem2  23286  ovolicc2lem4  23288  ovolicc2lem5  23289  ismbl  23294  dyadmbllem  23367  dyadmbl  23368  ismbf1  23393  isi1f  23441  isibl  23532  isuc1p  23900  ismon1p  23902  radcnvle  24174  abelthlem2  24186  abelthlem7a  24191  atans  24657  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgambdd  24763  wilthlem2  24795  wilthlem3  24796  ftalem3  24801  sqff1o  24908  dvdsmulf1o  24920  lgslem2  25023  lgslem3  25024  lgsfcl2  25028  rpvmasumlem  25176  dchrvmaeq0  25193  dchrisum0re  25202  pntlem3  25298  axcontlem2  25845  lfgredgge2  26019  uspgredg2vlem  26115  uspgredg2v  26116  usgredg2vlem1  26117  usgredg2vlem2  26118  ushgredgedg  26121  ushgredgedgloop  26123  uhgrspan1  26195  upgrreslem  26196  umgrreslem  26197  isfusgr  26210  nbupgrres  26266  iscusgr  26314  cusgrexilem2  26338  cusgrfilem2  26352  vtxdginducedm1lem4  26438  iswspthn  26736  wlknwwlksnfun  26774  wlknwwlksninj  26775  wlkwwlkfun  26781  wlkwwlkinj  26782  wlkwwlksur  26783  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextsur  26795  wwlksnextproplem3  26806  clwwlksel  26914  clwwlksf  26915  clwwlksf1  26917  clwlksfclwwlk1hashn  26959  clwlksfoclwwlk  26963  clwlksf1clwwlklem0  26964  frgrwopreglem3  27178  frgrwopreglem5lem  27184  frgrwopreglem5  27185  extwwlkfab  27223  isablo  27400  iscbn  27720  hcau  28041  issh  28065  isch  28079  elcnop  28716  ellnop  28717  elbdop  28719  elhmop  28732  elcnfn  28741  ellnfn  28742  isst  29072  ishst  29073  ela  29198  isomnd  29701  isslmd  29755  isorng  29799  iscref  29911  isrrext  30044  ispisys  30215  isldsys  30219  isros  30231  issros  30238  oddpwdc  30416  eulerpartleme  30425  eulerpartlemo  30427  eulerpartlemd  30428  eulerpartlemt0  30431  eulerpartlemf  30432  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemmf  30437  eulerpartlemgvv  30438  eulerpartlemgs2  30442  eulerpartlemn  30443  elprob  30471  ballotlemelo  30549  ballotleme  30558  bnj1152  31066  bnj1280  31088  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem1  31173  ispconn  31205  issconn  31208  cvmsiota  31259  cvmlift2lem12  31296  rdgprc0  31699  elwlim  31769  elwlimOLD  31770  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  topdifinffinlem  33195  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  isprrngo  33849  rabeqel  34019  toycom  34260  isopos  34467  isoml  34525  isatl  34586  iscvlat  34610  ishlat1  34639  cdlemm10N  36407  dihglblem2N  36583  lcfl1lem  36780  lcfls1lem  36823  mapdordlem1a  36923  mapdordlem1  36925  pellqrex  37443  islnm  37647  pwssplit4  37659  islnr  37681  fnlimcnv  39899  stoweidlem14  40231  stoweidlem16  40233  stoweidlem37  40254  stoweidlem48  40265  stoweidlem51  40268  stoweidlem59  40276  salexct  40552  salexct2  40557  salexct3  40560  salgencntex  40561  salgensscntex  40562  ovn0lem  40779  opnvonmbllem1  40846  ovolval5lem2  40867  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  smfresal  40995  smfmullem2  40999  smfpimbor1lem1  41005  smfpimbor1lem2  41006  smfinflem  41023  iseven  41541  isodd  41542  m1expevenALTV  41560  iseven2  41564  isodd3  41565  odd2np1ALTV  41585  opoeALTV  41594  opeoALTV  41595  isgbe  41639  isgbow  41640  isgbo  41641  sprsymrelfo  41747  0nodd  41810  1odd  41811  2nodd  41812  iscmgmALT  41860  issgrpALT  41861  iscsgrpALT  41862  isrng  41876  1neven  41932  2zlidl  41934  2zrngamgm  41939  2zrngagrp  41943  2zrngmmgm  41946  2zrngnmrid  41950