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

Theorem elimasn 5932
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 𝐵 ∈ V
elimasn.2 𝐶 ∈ V
Assertion
Ref Expression
elimasn (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)

Proof of Theorem elimasn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elimasn.2 . . 3 𝐶 ∈ V
2 breq2 5046 . . 3 (𝑥 = 𝐶 → (𝐵𝐴𝑥𝐵𝐴𝐶))
3 elimasn.1 . . . 4 𝐵 ∈ V
4 imasng 5929 . . . 4 (𝐵 ∈ V → (𝐴 “ {𝐵}) = {𝑥𝐵𝐴𝑥})
53, 4ax-mp 5 . . 3 (𝐴 “ {𝐵}) = {𝑥𝐵𝐴𝑥}
61, 2, 5elab2 3645 . 2 (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶)
7 df-br 5043 . 2 (𝐵𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
86, 7bitri 278 1 (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2114  {cab 2800  Vcvv 3469  {csn 4539  cop 4545   class class class wbr 5042  cima 5535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-sep 5179  ax-nul 5186  ax-pr 5307
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4266  df-if 4440  df-sn 4540  df-pr 4542  df-op 4546  df-br 5043  df-opab 5105  df-xp 5538  df-cnv 5540  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545
This theorem is referenced by:  elimasng  5933  dfco2  6076  dfco2a  6077  ressn  6114  funfvima3  6981  frxp  7807  marypha1lem  8885  gsum2dlem1  19081  gsum2dlem2  19082  gsum2d  19083  gsum2d2  19085  ovoliunlem1  24104  iunsnima  30377  dfcnv2  30430  gsummpt2co  30717  gsummpt2d  30718  dmscut  33346  scutf  33347  funpartfun  33478  areaquad  40096  dffrege76  40571  frege97  40592  frege98  40593  frege109  40604  frege110  40605  frege131  40626  frege133  40628
  Copyright terms: Public domain W3C validator