Theorem elimasn 6092

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 6090, remove, and relabel elimasn1 6090 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 6091	. 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))
4	1, 2, 3	mp2an 704	1 ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)

Syntax hints:   ↔ wb 209   ∈ wcel 2143  Vcvv 3455  {csn 4589  ⟨cop 4595   “ cima 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674

This theorem is referenced by:  dfco2  6246  dfco2a  6247  ressn  6286  funfvima3  7234  frxp  8118  frxp2  8136  frxp3  8143  marypha1lem  9389  gsum2dlem1  20035  gsum2dlem2  20036  gsum2d  20037  gsum2d2  20039  ovoliunlem1  25661  dmcuts  27984  cutsf  27985  iunsnima  32963  dfcnv2  33020  gsummpt2co  33368  gsummpt2d  33369  gsumfs2d  33381  funpartfun  36435  areaquad  43963  dffrege76  44685  frege97  44706  frege98  44707  frege109  44718  frege110  44719  frege131  44740  frege133  44742