Theorem elimasng 6046

Description: Membership in an image of a singleton. (Contributed by Raph Levien, 21-Oct-2006.) TODO: replace existing usages by usages of elimasng1 6044, remove, and relabel elimasng1 6044 to "elimasng".

Assertion

Ref	Expression
elimasng	⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))

Proof of Theorem elimasng

Step	Hyp	Ref	Expression
1		elimasng1 6044	. 2 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ 𝐵𝐴𝐶))
2		df-br 5097	. 2 ⊢ (𝐵𝐴𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)
3	1, 2	bitrdi 287	1 ⊢ ((𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  {csn 4578  ⟨cop 4584   class class class wbr 5096   “ cima 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635

This theorem is referenced by:  elimasn  6047  inimasn  6112  dffv3  6828  fvimacnv  6996  fvrnressn  7104  elecg  8677  imasnopn  23632  imasncld  23633  imasncls  23634  ustelimasn  24165  blval2  24504  elbl4  24505  scutval  27768  iunsnima2  32646  1stpreimas  32734  opelco3  35918  funpartfv  36088  eltail  36517  elecALTV  38403  brtrclfv2  43910  frege77d  43929  dfafv23  47441