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 4268 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐶 ↔ {𝐴} ⊆ 𝐶)) | |
2 | snssg 4268 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ 𝐶 ↔ {𝐵} ⊆ 𝐶)) | |
3 | 1, 2 | bi2anan9 913 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ ({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶))) |
4 | unss 3749 | . . 3 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶) | |
5 | df-pr 4128 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
6 | 5 | sseq1i 3592 | . . 3 ⊢ ({𝐴, 𝐵} ⊆ 𝐶 ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶) |
7 | 4, 6 | bitr4i 266 | . 2 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
8 | 3, 7 | syl6bb 275 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∈ wcel 1977 ∪ cun 3538 ⊆ wss 3540 {csn 4125 {cpr 4127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 df-sn 4126 df-pr 4128 |
This theorem is referenced by: prss 4291 prssi 4293 prsspwg 4295 ssprss 4296 prelpw 4841 lspprss 18813 lspvadd 18917 topgele 20549 umgredgprv 25773 usgraedgprv 25905 usgraedgrnv 25906 usgraedg4 25916 2trllemH 26082 2trllemE 26083 dihmeetlem2N 35606 fourierdlem20 39020 fourierdlem50 39049 fourierdlem54 39053 fourierdlem64 39063 fourierdlem76 39075 omeunle 39406 usgredgprvALT 40422 dfnbgr2 40561 nbuhgr 40565 uhgrnbgr0nb 40576 21wlkdlem6 41138 11wlkdlem2 41305 |
Copyright terms: Public domain | W3C validator |