![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prssg | Structured version Visualization version GIF version |
Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 22-Mar-2006.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Ref | Expression |
---|---|
prssg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssg 4678 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐶 ↔ {𝐴} ⊆ 𝐶)) | |
2 | snssg 4678 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ 𝐶 ↔ {𝐵} ⊆ 𝐶)) | |
3 | 1, 2 | bi2anan9 638 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ ({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶))) |
4 | unss 4111 | . . 3 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶) | |
5 | df-pr 4528 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
6 | 5 | sseq1i 3943 | . . 3 ⊢ ({𝐴, 𝐵} ⊆ 𝐶 ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶) |
7 | 4, 6 | bitr4i 281 | . 2 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
8 | 3, 7 | syl6bb 290 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2111 ∪ cun 3879 ⊆ wss 3881 {csn 4525 {cpr 4527 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 |
This theorem is referenced by: prss 4713 prssi 4714 prsspwg 4716 ssprss 4717 prelpw 5304 hashdmpropge2 13837 lspvadd 19861 umgredgprv 26900 usgredgprvALT 26985 dfnbgr2 27127 nbuhgr 27133 uhgrnbgr0nb 27144 2wlkdlem6 27717 1wlkdlem2 27923 coss0 35879 dihmeetlem2N 38595 mnuprdlem2 40981 fourierdlem20 42769 fourierdlem50 42798 fourierdlem54 42802 fourierdlem64 42812 fourierdlem76 42824 omeunle 43155 |
Copyright terms: Public domain | W3C validator |