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

Theorem prssg 4844
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 4808 . . 3 (𝐴𝑉 → (𝐴𝐶 ↔ {𝐴} ⊆ 𝐶))
2 snssg 4808 . . 3 (𝐵𝑊 → (𝐵𝐶 ↔ {𝐵} ⊆ 𝐶))
31, 2bi2anan9 637 . 2 ((𝐴𝑉𝐵𝑊) → ((𝐴𝐶𝐵𝐶) ↔ ({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶)))
4 unss 4213 . . 3 (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶)
5 df-pr 4651 . . . 4 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
65sseq1i 4037 . . 3 ({𝐴, 𝐵} ⊆ 𝐶 ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶)
74, 6bitr4i 278 . 2 (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
83, 7bitrdi 287 1 ((𝐴𝑉𝐵𝑊) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2108  cun 3974  wss 3976  {csn 4648  {cpr 4650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651
This theorem is referenced by:  prss  4845  prssi  4846  prsspwg  4848  ssprss  4849  prelpw  5466  hashdmpropge2  14532  lspvadd  21118  umgredgprv  29142  usgredgprvALT  29230  dfnbgr2  29372  nbuhgr  29378  uhgrnbgr0nb  29389  2wlkdlem6  29964  1wlkdlem2  30170  coss0  38435  dihmeetlem2N  41256  mnuprdlem2  44242  fourierdlem20  46048  fourierdlem50  46077  fourierdlem54  46081  fourierdlem64  46091  fourierdlem76  46103  omeunle  46437  dfclnbgr2  47697  dfsclnbgr2  47718  dfvopnbgr2  47725
  Copyright terms: Public domain W3C validator