MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrab2 Structured version   Unicode version

Theorem elrab2 3263
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
StepHypRef Expression
1 elrab2.2 . . 3  |-  C  =  { x  e.  B  |  ph }
21eleq2i 2545 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3261 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 249 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115
This theorem is referenced by:  elrabsf  3370  pwnss  4612  fvmpti  5949  fvmptss2  5969  tfis  6673  elom  6687  oawordeulem  7203  oeeulem  7250  mapfienlem1  7864  mapfienlem3  7866  mapfien  7867  ordtypelem2  7944  ordtypelem3  7945  ordtypelem9  7951  wemapso2OLD  7977  wemapso2lem  7978  inf3lema  8041  oemapvali  8103  mapfienOLD  8138  tz9.12lem3  8207  cofsmo  8649  enfin2i  8701  fin23lem28  8720  isf32lem6  8738  hsmexlem4  8809  zorn2lem2  8877  pwfseqlem1  9036  pwfseqlem3  9038  nqereu  9307  elz  10866  zsupss  11171  rpnnen1lem5  11212  elrp  11222  repos  11621  sqrlem1  13039  sqrlem2  13040  sqrlem6  13044  sqrlem7  13045  ello1  13301  elo1  13312  rlimrege0  13365  divalglem2  13912  divalglem4  13913  divalglem5  13914  divalglem9  13918  divalglem10  13919  bitsfzolem  13943  gcdcllem1  14008  gcdcllem2  14009  gcdcllem3  14010  bezoutlem1  14035  bezoutlem3  14037  bezoutlem4  14038  isprm  14078  maxprmfct  14113  phimullem  14168  eulerthlem1  14170  eulerthlem2  14171  pclem  14221  pcprecl  14222  pcprendvds  14223  infpn2  14290  prmreclem1  14293  prmreclem2  14294  prmreclem3  14295  prmreclem5  14297  1arith  14304  elgz  14308  4sqlem13  14334  4sqlem17  14338  4sqlem18  14339  vdwnnlem2  14373  vdwnnlem3  14374  ramtlecl  14377  isdrs  15421  istos  15522  islat  15534  isclat  15596  isdlat  15680  istsr  15704  gsumvallem2  15823  isgrp  15871  elnmz  16045  gastacl  16152  gastacos  16153  symgfixelq  16263  psgneldm  16334  sylow1lem2  16425  sylow1lem4  16427  sylow2alem1  16443  sylow2alem2  16444  efgsdm  16554  iscmn  16611  iscyg  16685  iscyggen  16686  dprdw  16846  dprdwOLD  16852  ablfacrplem  16918  ablfacrp  16919  ablfac1c  16924  ablfac1eu  16926  pgpfaclem1  16934  ablfaclem3  16940  ablfac2  16942  issrg  16961  isrng  17004  iscrng  17007  isdrng  17200  islmod  17316  islvec  17550  lspsolvlem  17588  lbsextlem1  17604  lbsextlem3  17606  lbsextlem4  17607  islpir  17696  isnzr  17706  isrrg  17735  isdomn  17742  isassa  17763  psrbag  17812  psrbaglefi  17822  psrbaglefiOLD  17823  psrbagconcl  17824  psrbagconf1o  17825  gsumbagdiaglem  17826  mplelbas  17886  mplelbasOLD  17888  isphl  18458  pjdm  18533  ishil  18544  frlmssuvc1  18620  frlmssuvc2  18621  frlmssuvc1OLD  18622  frlmssuvc2OLD  18623  frlmsslsp  18624  frlmsslspOLD  18625  gsummatr01lem1  18952  gsummatr01lem4  18955  gsummatr01  18956  mretopd  19387  neipeltop  19424  isperf  19446  ist0  19615  ist1  19616  ishaus  19617  iscnrm  19618  isreg  19627  isnrm  19630  ispnrm  19634  iscmp  19682  hauscmplem  19700  iscon  19708  concompss  19728  is1stc  19736  islly  19763  isnlly  19764  dfac14lem  19881  ishmeo  20023  ptcmplem3  20317  ptcmplem4  20318  istmd  20336  istgp  20339  tgpconcompeqg  20373  tgpt0  20380  divstgpopn  20381  istrg  20429  istdrg  20431  istlm  20450  istvc  20457  iscusp  20565  imasdsf1olem  20639  isxms  20713  isms  20715  blcld  20771  prdsxmslem2  20795  isngp  20879  isnrg  20932  isnlm  20947  icccmplem1  21090  icccmplem2  21091  isclm  21327  iscph  21380  isbn  21540  iscms  21547  ivthlem1  21626  ivthlem2  21627  ivthlem3  21628  elovolm  21649  ovolicc2lem2  21692  ovolicc2lem4  21694  ovolicc2lem5  21695  ismbl  21700  dyadmbllem  21771  dyadmbl  21772  ismbf1  21796  isi1f  21844  isibl  21935  isuc1p  22304  ismon1p  22306  radcnvle  22577  abelthlem2  22589  abelthlem7a  22594  atans  23017  wilthlem2  23099  wilthlem3  23100  ftalem3  23104  sqff1o  23212  dvdsmulf1o  23226  lgslem2  23328  lgslem3  23329  lgsfcl2  23333  rpvmasumlem  23428  dchrvmaeq0  23445  dchrisum0re  23454  pntlem3  23550  axcontlem2  23972  edg  24057  usgraidx2vlem1  24095  usgraidx2vlem2  24096  cusgraexi  24172  cusgrafilem2  24184  wlknwwlknfun  24414  wlknwwlkninj  24415  wlkiswwlkfun  24421  wlkiswwlkinj  24422  wwlkextfun  24433  wwlkextproplem3  24447  clwwlkel  24497  clwwlkf  24498  clwwlkf1  24500  clwlkfoclwwlk  24549  clwlkf1clwwlklem3  24552  frgrawopreglem3  24751  extwwlkfab  24795  isablo  24989  iscbn  25484  hcau  25805  issh  25829  isch  25844  elcnop  26480  ellnop  26481  elbdop  26483  elhmop  26496  elcnfn  26505  ellnfn  26506  isst  26836  ishst  26837  ela  26962  isomnd  27381  isslmd  27435  isorng  27480  isrrext  27645  oddpwdc  27961  eulerpartleme  27970  eulerpartlemo  27972  eulerpartlemd  27973  eulerpartlemt0  27976  eulerpartlemf  27977  eulerpartlemt  27978  eulerpartlemr  27981  eulerpartlemmf  27982  eulerpartlemgvv  27983  eulerpartlemgs2  27987  eulerpartlemn  27988  elprob  28016  ballotlemelo  28094  ballotleme  28103  lgamgulmlem2  28240  lgamgulmlem3  28241  lgamgulmlem5  28243  lgambdd  28247  subfacp1lem3  28294  subfacp1lem5  28296  erdszelem1  28303  ispcon  28336  isscon  28339  cvmsiota  28390  cvmlift2lem12  28427  rdgprc0  28831  elwlim  28984  neibastop1  29808  neibastop2lem  29809  neibastop2  29810  isprrngo  30078  pellqrex  30447  islnm  30655  pwssplit4  30667  islnr  30692  hashgcdlem  30790  stoweidlem14  31342  stoweidlem16  31344  stoweidlem37  31365  stoweidlem48  31376  stoweidlem51  31379  stoweidlem59  31387  usgedgvadf1lem1  31908  usgedgvadf1lem2  31909  usgedgvadf1ALTlem1  31911  usgedgvadf1ALTlem2  31912  issgrp  31954  iscmgmALT2  32006  issgrpALT2  32007  iscsgrpALT2  32008  isrng0  32013  bnj1152  33151  bnj1280  33173  toycom  33788  isopos  33995  isoml  34053  isatl  34114  iscvlat  34138  ishlat1  34167  cdlemm10N  35933  dihglblem2N  36109  lcfl1lem  36306  lcfls1lem  36349  mapdordlem1a  36449  mapdordlem1  36451
  Copyright terms: Public domain W3C validator