Theorem elimasn 6110

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 6108, remove, and relabel elimasn1 6108 to "elimasn".

Hypotheses

Ref	Expression
elimasn.1	⊢ 𝐵 ∈ V
elimasn.2	⊢ 𝐶 ∈ V

Assertion

Ref	Expression
elimasn	⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)

Proof of Theorem elimasn

Step	Hyp	Ref	Expression
1		elimasn.1	. 2 ⊢ 𝐵 ∈ V
2		elimasn.2	. 2 ⊢ 𝐶 ∈ V
3		elimasng 6109	. 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
4	1, 2, 3	mp2an 692	1 ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2106  Vcvv 3478  {csn 4631  ⟨cop 4637   “ cima 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702

This theorem is referenced by:  elimasngOLD  6111  dfco2  6267  dfco2a  6268  ressn  6307  funfvima3  7256  frxp  8150  frxp2  8168  frxp3  8175  marypha1lem  9471  gsum2dlem1  20003  gsum2dlem2  20004  gsum2d  20005  gsum2d2  20007  ovoliunlem1  25551  dmscut  27871  scutf  27872  iunsnima  32638  dfcnv2  32693  gsummpt2co  33034  gsummpt2d  33035  gsumfs2d  33041  funpartfun  35925  areaquad  43205  dffrege76  43929  frege97  43950  frege98  43951  frege109  43962  frege110  43963  frege131  43984  frege133  43986