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

Theorem elimasng 5193
Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.)
Assertion
Ref Expression
elimasng  |-  ( ( B  e.  V  /\  C  e.  W )  ->  ( C  e.  ( A " { B } )  <->  <. B ,  C >.  e.  A ) )

Proof of Theorem elimasng
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sneq 3977 . . . . 5  |-  ( y  =  B  ->  { y }  =  { B } )
21imaeq2d 5167 . . . 4  |-  ( y  =  B  ->  ( A " { y } )  =  ( A
" { B }
) )
32eleq2d 2513 . . 3  |-  ( y  =  B  ->  (
z  e.  ( A
" { y } )  <->  z  e.  ( A " { B } ) ) )
4 opeq1 4165 . . . 4  |-  ( y  =  B  ->  <. y ,  z >.  =  <. B ,  z >. )
54eleq1d 2512 . . 3  |-  ( y  =  B  ->  ( <. y ,  z >.  e.  A  <->  <. B ,  z
>.  e.  A ) )
63, 5bibi12d 323 . 2  |-  ( y  =  B  ->  (
( z  e.  ( A " { y } )  <->  <. y ,  z >.  e.  A
)  <->  ( z  e.  ( A " { B } )  <->  <. B , 
z >.  e.  A ) ) )
7 eleq1 2516 . . 3  |-  ( z  =  C  ->  (
z  e.  ( A
" { B }
)  <->  C  e.  ( A " { B }
) ) )
8 opeq2 4166 . . . 4  |-  ( z  =  C  ->  <. B , 
z >.  =  <. B ,  C >. )
98eleq1d 2512 . . 3  |-  ( z  =  C  ->  ( <. B ,  z >.  e.  A  <->  <. B ,  C >.  e.  A ) )
107, 9bibi12d 323 . 2  |-  ( z  =  C  ->  (
( z  e.  ( A " { B } )  <->  <. B , 
z >.  e.  A )  <-> 
( C  e.  ( A " { B } )  <->  <. B ,  C >.  e.  A ) ) )
11 vex 3047 . . 3  |-  y  e. 
_V
12 vex 3047 . . 3  |-  z  e. 
_V
1311, 12elimasn 5192 . 2  |-  ( z  e.  ( A " { y } )  <->  <. y ,  z >.  e.  A )
146, 10, 13vtocl2g 3110 1  |-  ( ( B  e.  V  /\  C  e.  W )  ->  ( C  e.  ( A " { B } )  <->  <. B ,  C >.  e.  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1443    e. wcel 1886   {csn 3967   <.cop 3973   "cima 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-xp 4839  df-cnv 4841  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846
This theorem is referenced by:  elimasni  5194  eliniseg  5196  inimasn  5252  elpredim  5391  elpredg  5393  dffv3  5859  fvimacnv  5995  fvrnressn  6077  elecg  7399  imasnopn  20698  imasncld  20699  imasncls  20700  ustelimasn  21230  blval2  21570  elbl4  21571  1stpreimas  28279  opelco3  30413  funpartfv  30705  eltail  31023  brtrclfv2  36313  frege77d  36332
  Copyright terms: Public domain W3C validator