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

Theorem elimasn 5631
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 4788 . . 3 (𝑥 = 𝐶 → (𝐵𝐴𝑥𝐵𝐴𝐶))
3 elimasn.1 . . . 4 𝐵 ∈ V
4 imasng 5628 . . . 4 (𝐵 ∈ V → (𝐴 “ {𝐵}) = {𝑥𝐵𝐴𝑥})
53, 4ax-mp 5 . . 3 (𝐴 “ {𝐵}) = {𝑥𝐵𝐴𝑥}
61, 2, 5elab2 3503 . 2 (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶)
7 df-br 4785 . 2 (𝐵𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
86, 7bitri 264 1 (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1630  wcel 2144  {cab 2756  Vcvv 3349  {csn 4314  cop 4320   class class class wbr 4784  cima 5252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rex 3066  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-br 4785  df-opab 4845  df-xp 5255  df-cnv 5257  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262
This theorem is referenced by:  elimasng  5632  dfco2  5778  dfco2a  5779  ressn  5815  funfvima3  6637  frxp  7437  marypha1lem  8494  gsum2dlem1  18575  gsum2dlem2  18576  gsum2d  18577  gsum2d2  18579  ovoliunlem1  23489  iunsnima  29762  dfcnv2  29810  gsummpt2co  30114  gsummpt2d  30115  dmscut  32249  scutf  32250  funpartfun  32381  areaquad  38321  dffrege76  38752  frege97  38773  frege98  38774  frege109  38785  frege110  38786  frege131  38807  frege133  38809
  Copyright terms: Public domain W3C validator