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

Theorem elrab2 3096
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 2502 . 2  |-  ( A  e.  C  <->  A  e.  { x  e.  B  |  ph } )
3 elrab2.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
43elrab 3094 . 2  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
52, 4bitri 242 1  |-  ( A  e.  C  <->  ( A  e.  B  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   {crab 2711
This theorem is referenced by:  elrabsf  3201  pwnss  4368  tfis  4837  elom  4851  fvmpti  5808  fvmptss2  5827  oawordeulem  6800  oeeulem  6847  ordtypelem2  7491  ordtypelem3  7492  ordtypelem9  7498  wemapso2  7524  inf3lema  7582  oemapvali  7643  mapfien  7656  tz9.12lem3  7718  cofsmo  8154  enfin2i  8206  fin23lem28  8225  isf32lem6  8243  hsmexlem4  8314  zorn2lem2  8382  pwfseqlem1  8538  pwfseqlem3  8540  nqereu  8811  elz  10289  zsupss  10570  rpnnen1lem5  10609  elrp  10619  repos  11006  sqrlem1  12053  sqrlem2  12054  sqrlem6  12058  sqrlem7  12059  ello1  12314  elo1  12325  rlimrege0  12378  divalglem2  12920  divalglem4  12921  divalglem5  12922  divalglem9  12926  divalglem10  12927  bitsfzolem  12951  gcdcllem1  13016  gcdcllem2  13017  gcdcllem3  13018  bezoutlem1  13043  bezoutlem3  13045  bezoutlem4  13046  isprm  13086  maxprmfct  13118  phimullem  13173  eulerthlem1  13175  eulerthlem2  13176  pclem  13217  pcprecl  13218  pcprendvds  13219  infpn2  13286  prmreclem1  13289  prmreclem2  13290  prmreclem3  13291  prmreclem5  13293  1arith  13300  elgz  13304  4sqlem13  13330  4sqlem17  13334  4sqlem18  13335  vdwnnlem2  13369  vdwnnlem3  13370  ramtlecl  13373  isdrs  14396  istos  14469  islat  14481  isclat  14543  isdlat  14624  istsr  14654  isla  14670  gsumvallem2  14777  isgrp  14821  elnmz  14984  gastacl  15091  gastacos  15092  sylow1lem2  15238  sylow1lem4  15240  sylow2alem1  15256  sylow2alem2  15257  efgsdm  15367  iscmn  15424  iscyg  15494  iscyggen  15495  dprdw  15573  ablfacrplem  15628  ablfacrp  15629  ablfac1c  15634  ablfac1eu  15636  pgpfaclem1  15644  ablfaclem3  15650  ablfac2  15652  isrng  15673  iscrng  15676  isdrng  15844  islmod  15959  islvec  16181  lspsolvlem  16219  lbsextlem1  16235  lbsextlem3  16237  lbsextlem4  16238  islpir  16325  isnzr  16335  isrrg  16353  isdomn  16359  isassa  16380  psrbag  16436  psrbaglefi  16442  psrbagconcl  16443  psrbagconf1o  16444  gsumbagdiaglem  16445  mplelbas  16499  isphl  16864  pjdm  16939  ishil  16950  mretopd  17161  neipeltop  17198  isperf  17220  ist0  17389  ist1  17390  ishaus  17391  iscnrm  17392  isreg  17401  isnrm  17404  ispnrm  17408  iscmp  17456  hauscmplem  17474  iscon  17481  concompss  17501  is1stc  17509  islly  17536  isnlly  17537  dfac14lem  17654  ishmeo  17796  ptcmplem3  18090  ptcmplem4  18091  istmd  18109  istgp  18112  tgpconcompeqg  18146  tgpt0  18153  divstgpopn  18154  istrg  18198  istdrg  18200  istlm  18219  istvc  18226  iscusp  18334  imasdsf1olem  18408  isxms  18482  isms  18484  blcld  18540  prdsxmslem2  18564  isngp  18648  isnrg  18701  isnlm  18716  icccmplem1  18858  icccmplem2  18859  isclm  19094  iscph  19138  isbn  19296  iscms  19303  ivthlem1  19353  ivthlem2  19354  ivthlem3  19355  elovolm  19376  ovolicc2lem2  19419  ovolicc2lem4  19421  ovolicc2lem5  19422  ismbl  19427  dyadmbllem  19496  dyadmbl  19497  ismbf1  19521  isi1f  19569  isibl  19660  isuc1p  20068  ismon1p  20070  radcnvle  20341  abelthlem2  20353  abelthlem7a  20358  atans  20775  wilthlem2  20857  wilthlem3  20858  ftalem3  20862  sqff1o  20970  dvdsmulf1o  20984  lgslem2  21086  lgslem3  21087  lgsfcl2  21091  rpvmasumlem  21186  dchrvmaeq0  21203  dchrisum0re  21212  pntlem3  21308  usgraidx2vlem1  21415  usgraidx2vlem2  21416  cusgraexi  21482  cusgrafilem2  21494  isablo  21876  iscbn  22371  hcau  22691  issh  22715  isch  22730  elcnop  23365  ellnop  23366  elbdop  23368  elhmop  23381  elcnfn  23390  ellnfn  23391  isst  23721  ishst  23722  ela  23847  isofld  24240  isarchi  24257  elprob  24672  ballotlemelo  24750  ballotleme  24759  lgamgulmlem2  24819  lgamgulmlem3  24820  lgamgulmlem5  24822  lgambdd  24826  subfacp1lem3  24873  subfacp1lem5  24875  erdszelem1  24882  ispcon  24915  isscon  24918  cvmsiota  24969  cvmlift2lem12  25006  rdgprc0  25426  elwlim  25579  axcontlem2  25909  neibastop1  26402  neibastop2lem  26403  neibastop2  26404  isprrngo  26674  pellqrex  26956  islnm  27166  pwssplit4  27182  frlmssuvc1  27237  frlmssuvc2  27238  frlmsslsp  27239  islnr  27306  psgneldm  27417  hashgcdlem  27507  stoweidlem14  27753  stoweidlem16  27755  stoweidlem37  27776  stoweidlem48  27787  stoweidlem51  27790  stoweidlem59  27798  frgrawopreglem3  28509  bnj1152  29441  bnj1280  29463  toycom  29844  isopos  30052  isoml  30110  isatl  30171  iscvlat  30195  ishlat1  30224  cdlemm10N  31990  dihglblem2N  32166  lcfl1lem  32363  lcfls1lem  32406  mapdordlem1a  32506  mapdordlem1  32508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960
  Copyright terms: Public domain W3C validator