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

Theorem elimasn 5187
Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Hypotheses
Ref Expression
elimasn.1  |-  B  e. 
_V
elimasn.2  |-  C  e. 
_V
Assertion
Ref Expression
elimasn  |-  ( C  e.  ( A " { B } )  <->  <. B ,  C >.  e.  A )

Proof of Theorem elimasn
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elimasn.2 . . 3  |-  C  e. 
_V
2 breq2 4289 . . 3  |-  ( x  =  C  ->  ( B A x  <->  B A C ) )
3 elimasn.1 . . . 4  |-  B  e. 
_V
4 imasng 5184 . . . 4  |-  ( B  e.  _V  ->  ( A " { B }
)  =  { x  |  B A x }
)
53, 4ax-mp 5 . . 3  |-  ( A
" { B }
)  =  { x  |  B A x }
61, 2, 5elab2 3102 . 2  |-  ( C  e.  ( A " { B } )  <->  B A C )
7 df-br 4286 . 2  |-  ( B A C  <->  <. B ,  C >.  e.  A )
86, 7bitri 249 1  |-  ( C  e.  ( A " { B } )  <->  <. B ,  C >.  e.  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369    e. wcel 1756   {cab 2423   _Vcvv 2966   {csn 3870   <.cop 3876   class class class wbr 4285   "cima 4835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pr 4524
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-br 4286  df-opab 4344  df-xp 4838  df-cnv 4840  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845
This theorem is referenced by:  elimasng  5188  dfco2  5330  dfco2a  5331  ressn  5366  funfvima3  5947  frxp  6677  marypha1lem  7675  gsum2dlem1  16447  gsum2dlem2  16448  gsum2d  16449  gsum2dOLD  16450  gsum2d2  16452  ovoliunlem1  20954  dfcnv2  25939  gsummpt2co  26196  funpartfun  27921  areaquad  29535
  Copyright terms: Public domain W3C validator