Theorem prss 4801

Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 23-Jul-2021.)

Hypotheses

Ref	Expression
prss.1	⊢ 𝐴 ∈ V
prss.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
prss	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prss

Step	Hyp	Ref	Expression
1		prss.1	. 2 ⊢ 𝐴 ∈ V
2		prss.2	. 2 ⊢ 𝐵 ∈ V
3		prssg 4800	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
4	1, 2, 3	mp2an 692	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3464   ⊆ wss 3931  {cpr 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948  df-sn 4607  df-pr 4609

This theorem is referenced by:  tpss  4818  uniintsn  4966  pwssun  5550  xpsspw  5793  dffv2  6979  fiint  9343  fiintOLD  9344  wunex2  10757  hashfun  14460  fun2dmnop0  14527  prdsle  17481  prdsless  17482  prdsleval  17496  pwsle  17511  acsfn2  17680  joinfval  18388  joindmss  18394  meetfval  18402  meetdmss  18408  clatl  18523  ipoval  18545  ipolerval  18547  eqgfval  19164  eqgval  19165  eqg0subg  19184  gaorb  19295  pmtrrn2  19446  efgcpbllema  19740  frgpuplem  19758  isnzr2hash  20484  thlle  21662  ltbval  22006  ltbwe  22007  opsrle  22010  opsrtoslem1  22018  isphtpc  24949  axlowdimlem4  28929  structgrssvtx  29008  structgrssiedg  29009  umgredg  29122  wlk1walk  29624  wlkonl1iedg  29650  wlkdlem2  29668  3wlkdlem6  30151  frcond2  30253  frcond3  30255  nfrgr2v  30258  frgr3vlem1  30259  frgr3vlem2  30260  2pthfrgrrn  30268  frgrncvvdeqlem2  30286  shincli  31348  chincli  31446  lsmsnorb  33411  quslsm  33425  coinfliprv  34520  altxpsspw  36000  mnurndlem1  44272  fourierdlem103  46205  fourierdlem104  46206  nnsum3primes4  47769  isubgr3stgrlem6  47950  grlimgrtrilem2  47974  gpgprismgr4cycllem8  48068