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

Step	Hyp	Ref	Expression
1		snssg 4745	. . 3 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐶 ↔ {𝐴} ⊆ 𝐶))
2		snssg 4745	. . 3 ⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ 𝐶 ↔ {𝐵} ⊆ 𝐶))
3	1, 2	bi2anan9 649	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ ({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶)))
4		unss 4145	. . 3 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶)
5		df-pr 4588	. . . 4 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
6	5	sseq1i 3967	. . 3 ⊢ ({𝐴, 𝐵} ⊆ 𝐶 ↔ ({𝐴} ∪ {𝐵}) ⊆ 𝐶)
7	4, 6	bitr4i 281	. 2 ⊢ (({𝐴} ⊆ 𝐶 ∧ {𝐵} ⊆ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
8	3, 7	bitrdi 290	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2145   ∪ cun 3905   ⊆ wss 3907  {csn 4585  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588

This theorem is referenced by:  prss  4781  prssi  4782  prsspwg  4784  ssprss  4785  prelpw  5418  hashdmpropge2  14510  lspvadd  21186  umgredgprv  29366  usgredgprvALT  29454  dfnbgr2  29596  nbuhgr  29602  uhgrnbgr0nb  29613  2wlkdlem6  30189  1wlkdlem2  30398  prssad  32785  prssbd  32786  tpssg  32793  coss0  39080  dihmeetlem2N  41935  mnuprdlem2  44847  fourierdlem20  46699  fourierdlem50  46728  fourierdlem54  46732  fourierdlem64  46742  fourierdlem76  46754  omeunle  47088  dfclnbgr2  48443  dfsclnbgr2  48466  dfvopnbgr2  48473  isubgr3stgrlem7  48592