MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prssg Structured version   Visualization version   GIF version

Theorem prssg 4780
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.)
Assertion
Ref Expression
prssg ((𝐴𝑉𝐵𝑊) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))

Proof of Theorem prssg
StepHypRef Expression
1 snssg 4745 . . 3 (𝐴𝑉 → (𝐴𝐶 ↔ {𝐴} ⊆ 𝐶))
2 snssg 4745 . . 3 (𝐵𝑊 → (𝐵𝐶 ↔ {𝐵} ⊆ 𝐶))
31, 2bi2anan9 638 . 2 ((𝐴𝑉𝐵𝑊) → ((𝐴𝐶𝐵𝐶) ↔ ({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶)))
4 unss 4145 . . 3 (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶)
5 df-pr 4590 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
65sseq1i 3973 . . 3 ({𝐴, 𝐵} ⊆ 𝐶 ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶)
74, 6bitr4i 278 . 2 (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
83, 7bitrdi 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