![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elimasn | Structured version Visualization version GIF version |
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 6043, remove, and relabel elimasn1 6043 to "elimasn". |
Ref | Expression |
---|---|
elimasn.1 | ⊢ 𝐵 ∈ V |
elimasn.2 | ⊢ 𝐶 ∈ V |
Ref | Expression |
---|---|
elimasn | ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elimasn.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | elimasn.2 | . 2 ⊢ 𝐶 ∈ V | |
3 | elimasng 6044 | . 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴)) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ (𝐶 ∈ (𝐴 “ {𝐵}) ↔ ⟨𝐵, 𝐶⟩ ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2107 Vcvv 3447 {csn 4590 ⟨cop 4596 “ cima 5640 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-br 5110 df-opab 5172 df-xp 5643 df-cnv 5645 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 |
This theorem is referenced by: elimasngOLD 6046 dfco2 6201 dfco2a 6202 ressn 6241 funfvima3 7190 frxp 8062 frxp2 8080 frxp3 8087 marypha1lem 9377 gsum2dlem1 19755 gsum2dlem2 19756 gsum2d 19757 gsum2d2 19759 ovoliunlem1 24889 dmscut 27179 scutf 27180 iunsnima 31590 dfcnv2 31645 gsummpt2co 31946 gsummpt2d 31947 funpartfun 34581 areaquad 41597 dffrege76 42303 frege97 42324 frege98 42325 frege109 42336 frege110 42337 frege131 42358 frege133 42360 |
Copyright terms: Public domain | W3C validator |