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