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

Theorem elimasn 6088
Description: Membership in an image of a singleton. (Contributed by NM, 15-Mar-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by BJ, 16-Oct-2024.) TODO: replace existing usages by usages of elimasn1 6086, remove, and relabel elimasn1 6086 to "elimasn".
Hypotheses
Ref Expression
elimasn.1 𝐵 ∈ V
elimasn.2 𝐶 ∈ V
Assertion
Ref Expression
elimasn (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)

Proof of Theorem elimasn
StepHypRef Expression
1 elimasn.1 . 2 𝐵 ∈ V
2 elimasn.2 . 2 𝐶 ∈ V
3 elimasng 6087 . 2 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
41, 2, 3mp2an 690 1 (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2106  Vcvv 3474  {csn 4628  cop 4634  cima 5679
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689
This theorem is referenced by:  elimasngOLD  6089  dfco2  6244  dfco2a  6245  ressn  6284  funfvima3  7237  frxp  8111  frxp2  8129  frxp3  8136  marypha1lem  9427  gsum2dlem1  19837  gsum2dlem2  19838  gsum2d  19839  gsum2d2  19841  ovoliunlem1  25018  dmscut  27309  scutf  27310  iunsnima  31842  dfcnv2  31896  gsummpt2co  32195  gsummpt2d  32196  funpartfun  34910  areaquad  41955  dffrege76  42680  frege97  42701  frege98  42702  frege109  42713  frege110  42714  frege131  42735  frege133  42737
  Copyright terms: Public domain W3C validator