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

Theorem elrab2 3054
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 2468 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3052 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 241 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   {crab 2670
This theorem is referenced by:  elrabsf  3159  pwnss  4325  tfis  4793  elom  4807  fvmpti  5764  fvmptss2  5783  oawordeulem  6756  oeeulem  6803  ordtypelem2  7444  ordtypelem3  7445  ordtypelem9  7451  wemapso2  7477  inf3lema  7535  oemapvali  7596  mapfien  7609  tz9.12lem3  7671  cofsmo  8105  enfin2i  8157  fin23lem28  8176  isf32lem6  8194  hsmexlem4  8265  zorn2lem2  8333  pwfseqlem1  8489  pwfseqlem3  8491  nqereu  8762  elz  10240  zsupss  10521  rpnnen1lem5  10560  elrp  10570  repos  10957  sqrlem1  12003  sqrlem2  12004  sqrlem6  12008  sqrlem7  12009  ello1  12264  elo1  12275  rlimrege0  12328  divalglem2  12870  divalglem4  12871  divalglem5  12872  divalglem9  12876  divalglem10  12877  bitsfzolem  12901  gcdcllem1  12966  gcdcllem2  12967  gcdcllem3  12968  bezoutlem1  12993  bezoutlem3  12995  bezoutlem4  12996  isprm  13036  maxprmfct  13068  phimullem  13123  eulerthlem1  13125  eulerthlem2  13126  pclem  13167  pcprecl  13168  pcprendvds  13169  infpn2  13236  prmreclem1  13239  prmreclem2  13240  prmreclem3  13241  prmreclem5  13243  1arith  13250  elgz  13254  4sqlem13  13280  4sqlem17  13284  4sqlem18  13285  vdwnnlem2  13319  vdwnnlem3  13320  ramtlecl  13323  isdrs  14346  istos  14419  islat  14431  isclat  14493  isdlat  14574  istsr  14604  isla  14620  gsumvallem2  14727  isgrp  14771  elnmz  14934  gastacl  15041  gastacos  15042  sylow1lem2  15188  sylow1lem4  15190  sylow2alem1  15206  sylow2alem2  15207  efgsdm  15317  iscmn  15374  iscyg  15444  iscyggen  15445  dprdw  15523  ablfacrplem  15578  ablfacrp  15579  ablfac1c  15584  ablfac1eu  15586  pgpfaclem1  15594  ablfaclem3  15600  ablfac2  15602  isrng  15623  iscrng  15626  isdrng  15794  islmod  15909  islvec  16131  lspsolvlem  16169  lbsextlem1  16185  lbsextlem3  16187  lbsextlem4  16188  islpir  16275  isnzr  16285  isrrg  16303  isdomn  16309  isassa  16330  psrbag  16386  psrbaglefi  16392  psrbagconcl  16393  psrbagconf1o  16394  gsumbagdiaglem  16395  mplelbas  16449  isphl  16814  pjdm  16889  ishil  16900  mretopd  17111  neipeltop  17148  isperf  17169  ist0  17338  ist1  17339  ishaus  17340  iscnrm  17341  isreg  17350  isnrm  17353  ispnrm  17357  iscmp  17405  hauscmplem  17423  iscon  17429  concompss  17449  is1stc  17457  islly  17484  isnlly  17485  dfac14lem  17602  ishmeo  17744  ptcmplem3  18038  ptcmplem4  18039  istmd  18057  istgp  18060  tgpconcompeqg  18094  tgpt0  18101  divstgpopn  18102  istrg  18146  istdrg  18148  istlm  18167  istvc  18174  iscusp  18282  imasdsf1olem  18356  isxms  18430  isms  18432  blcld  18488  prdsxmslem2  18512  isngp  18596  isnrg  18649  isnlm  18664  icccmplem1  18806  icccmplem2  18807  isclm  19042  iscph  19086  isbn  19244  iscms  19251  ivthlem1  19301  ivthlem2  19302  ivthlem3  19303  elovolm  19324  ovolicc2lem2  19367  ovolicc2lem4  19369  ovolicc2lem5  19370  ismbl  19375  dyadmbllem  19444  dyadmbl  19445  ismbf1  19471  isi1f  19519  isibl  19610  isuc1p  20016  ismon1p  20018  radcnvle  20289  abelthlem2  20301  abelthlem7a  20306  atans  20723  wilthlem2  20805  wilthlem3  20806  ftalem3  20810  sqff1o  20918  dvdsmulf1o  20932  lgslem2  21034  lgslem3  21035  lgsfcl2  21039  rpvmasumlem  21134  dchrvmaeq0  21151  dchrisum0re  21160  pntlem3  21256  usgraidx2vlem1  21363  usgraidx2vlem2  21364  cusgraexi  21430  cusgrafilem2  21442  isablo  21824  iscbn  22319  hcau  22639  issh  22663  isch  22678  elcnop  23313  ellnop  23314  elbdop  23316  elhmop  23329  elcnfn  23338  ellnfn  23339  isst  23669  ishst  23670  ela  23795  isofld  24188  isarchi  24205  elprob  24620  ballotlemelo  24698  ballotleme  24707  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem5  24770  lgambdd  24774  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem1  24830  ispcon  24863  isscon  24866  cvmsiota  24917  cvmlift2lem12  24954  rdgprc0  25364  axcontlem2  25808  neibastop1  26278  neibastop2lem  26279  neibastop2  26280  isprrngo  26550  pellqrex  26832  islnm  27043  pwssplit4  27059  frlmssuvc1  27114  frlmssuvc2  27115  frlmsslsp  27116  islnr  27183  psgneldm  27294  hashgcdlem  27384  stoweidlem14  27630  stoweidlem16  27632  stoweidlem37  27653  stoweidlem48  27664  stoweidlem51  27667  stoweidlem59  27675  frgrawopreglem3  28149  bnj1152  29073  bnj1280  29095  toycom  29455  isopos  29663  isoml  29721  isatl  29782  iscvlat  29806  ishlat1  29835  cdlemm10N  31601  dihglblem2N  31777  lcfl1lem  31974  lcfls1lem  32017  mapdordlem1a  32117  mapdordlem1  32119
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918
  Copyright terms: Public domain W3C validator