![]() |
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 4745 | . . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐶 ↔ {𝐴} ⊆ 𝐶)) | |
2 | snssg 4745 | . . 3 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ 𝐶 ↔ {𝐵} ⊆ 𝐶)) | |
3 | 1, 2 | bi2anan9 638 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ ({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶))) |
4 | unss 4145 | . . 3 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶) | |
5 | df-pr 4590 | . . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
6 | 5 | sseq1i 3973 | . . 3 ⊢ ({𝐴, 𝐵} ⊆ 𝐶 ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶) |
7 | 4, 6 | bitr4i 278 | . 2 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
8 | 3, 7 | bitrdi 287 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∪ cun 3909 ⊆ wss 3911 {csn 4587 {cpr 4589 |
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 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-un 3916 df-in 3918 df-ss 3928 df-sn 4588 df-pr 4590 |
This theorem is referenced by: prss 4781 prssi 4782 prsspwg 4784 ssprss 4785 prelpw 5404 hashdmpropge2 14388 lspvadd 20572 umgredgprv 28100 usgredgprvALT 28185 dfnbgr2 28327 nbuhgr 28333 uhgrnbgr0nb 28344 2wlkdlem6 28918 1wlkdlem2 29124 coss0 36987 dihmeetlem2N 39808 mnuprdlem2 42641 fourierdlem20 44454 fourierdlem50 44483 fourierdlem54 44487 fourierdlem64 44497 fourierdlem76 44509 omeunle 44843 |
Copyright terms: Public domain | W3C validator |