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

Theorem elrab2 2938
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 2360 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 2936 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 240 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   {crab 2560
This theorem is referenced by:  elrabsf  3042  pwnss  4192  tfis  4661  elom  4675  fvmpti  5617  fvmptss2  5635  oawordeulem  6568  oeeulem  6615  ordtypelem2  7250  ordtypelem3  7251  ordtypelem9  7257  wemapso2  7283  inf3lema  7341  oemapvali  7402  mapfien  7415  tz9.12lem3  7477  cofsmo  7911  enfin2i  7963  fin23lem28  7982  isf32lem6  8000  hsmexlem4  8071  zorn2lem2  8140  pwfseqlem1  8296  pwfseqlem3  8298  nqereu  8569  elz  10042  zsupss  10323  rpnnen1lem5  10362  elrp  10372  repos  10756  sqrlem1  11744  sqrlem2  11745  sqrlem6  11749  sqrlem7  11750  ello1  12005  elo1  12016  rlimrege0  12069  divalglem2  12610  divalglem4  12611  divalglem5  12612  divalglem9  12616  divalglem10  12617  bitsfzolem  12641  gcdcllem1  12706  gcdcllem2  12707  gcdcllem3  12708  bezoutlem1  12733  bezoutlem3  12735  bezoutlem4  12736  isprm  12776  maxprmfct  12808  phimullem  12863  eulerthlem1  12865  eulerthlem2  12866  pclem  12907  pcprecl  12908  pcprendvds  12909  infpn2  12976  prmreclem1  12979  prmreclem2  12980  prmreclem3  12981  prmreclem5  12983  1arith  12990  elgz  12994  4sqlem13  13020  4sqlem17  13024  4sqlem18  13025  vdwnnlem2  13059  vdwnnlem3  13060  ramtlecl  13063  isdrs  14084  istos  14157  islat  14169  isclat  14231  isdlat  14312  istsr  14342  isla  14358  gsumvallem2  14465  isgrp  14509  elnmz  14672  gastacl  14779  gastacos  14780  sylow1lem2  14926  sylow1lem4  14928  sylow2alem1  14944  sylow2alem2  14945  efgsdm  15055  iscmn  15112  iscyg  15182  iscyggen  15183  dprdw  15261  ablfacrplem  15316  ablfacrp  15317  ablfac1c  15322  ablfac1eu  15324  pgpfaclem1  15332  ablfaclem3  15338  ablfac2  15340  isrng  15361  iscrng  15364  isdrng  15532  islmod  15647  islvec  15873  lspsolvlem  15911  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  islpir  16017  isnzr  16027  isrrg  16045  isdomn  16051  isassa  16072  psrbag  16128  psrbaglefi  16134  psrbagconcl  16135  psrbagconf1o  16136  gsumbagdiaglem  16137  mplelbas  16191  isphl  16548  pjdm  16623  ishil  16634  mretopd  16845  isperf  16898  ist0  17064  ist1  17065  ishaus  17066  iscnrm  17067  isreg  17076  isnrm  17079  ispnrm  17083  iscmp  17131  hauscmplem  17149  iscon  17155  concompss  17175  is1stc  17183  islly  17210  isnlly  17211  dfac14lem  17327  ishmeo  17466  ptcmplem3  17764  ptcmplem4  17765  istmd  17773  istgp  17776  tgpconcompeqg  17810  tgpt0  17817  divstgpopn  17818  istrg  17862  istdrg  17864  istlm  17883  istvc  17890  imasdsf1olem  17953  isxms  18009  isms  18011  blcld  18067  prdsxmslem2  18091  isngp  18134  isnrg  18187  isnlm  18202  icccmplem1  18343  icccmplem2  18344  isclm  18578  iscph  18622  isbn  18776  iscms  18783  ivthlem1  18827  ivthlem2  18828  ivthlem3  18829  elovolm  18850  ovolicc2lem2  18893  ovolicc2lem4  18895  ovolicc2lem5  18896  ismbl  18901  dyadmbllem  18970  dyadmbl  18971  ismbf1  18997  isi1f  19045  isibl  19136  isuc1p  19542  ismon1p  19544  radcnvle  19812  abelthlem2  19824  abelthlem7a  19829  atans  20242  wilthlem2  20323  wilthlem3  20324  ftalem3  20328  sqff1o  20436  dvdsmulf1o  20450  lgslem2  20552  lgslem3  20553  lgsfcl2  20557  rpvmasumlem  20652  dchrvmaeq0  20669  dchrisum0re  20678  pntlem3  20774  isablo  20966  iscbn  21459  hcau  21779  issh  21803  isch  21818  elcnop  22453  ellnop  22454  elbdop  22456  elhmop  22469  elcnfn  22478  ellnfn  22479  isst  22809  ishst  22810  ela  22935  ballotlemelo  23062  ballotleme  23071  elprob  23627  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem1  23737  ispcon  23769  isscon  23772  cvmsiota  23823  cvmlift2lem12  23860  rdgprc0  24221  axcontlem2  24665  isibg2  26213  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  isprrngo  26778  pellqrex  27067  islnm  27278  pwssplit4  27294  frlmssuvc1  27349  frlmssuvc2  27350  frlmsslsp  27351  islnr  27418  psgneldm  27529  hashgcdlem  27619  stoweidlem16  27868  stoweidlem48  27900  stoweidlem51  27903  stoweidlem59  27911  bnj1152  29344  bnj1280  29366  toycom  29784  isopos  29992  isoml  30050  isatl  30111  iscvlat  30135  ishlat1  30164  cdlemm10N  31930  dihglblem2N  32106  lcfl1lem  32303  lcfls1lem  32346  mapdordlem1a  32446  mapdordlem1  32448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803
  Copyright terms: Public domain W3C validator