Theorem prss 4776

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 4775	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
4	1, 2, 3	mp2an 692	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583

This theorem is referenced by:  tpss  4793  uniintsn  4940  pwssun  5516  xpsspw  5758  dffv2  6929  fiint  9227  wunex2  10649  hashfun  14360  fun2dmnop0  14427  prdsle  17382  prdsless  17383  prdsleval  17397  pwsle  17413  acsfn2  17586  joinfval  18294  joindmss  18300  meetfval  18308  meetdmss  18314  clatl  18431  ipoval  18453  ipolerval  18455  eqgfval  19105  eqgval  19106  eqg0subg  19125  gaorb  19236  pmtrrn2  19389  efgcpbllema  19683  frgpuplem  19701  isnzr2hash  20452  thlle  21652  ltbval  21998  ltbwe  21999  opsrle  22002  opsrtoslem1  22010  isphtpc  24949  axlowdimlem4  29018  structgrssvtx  29097  structgrssiedg  29098  umgredg  29211  wlk1walk  29712  wlkonl1iedg  29737  wlkdlem2  29755  3wlkdlem6  30240  frcond2  30342  frcond3  30344  nfrgr2v  30347  frgr3vlem1  30348  frgr3vlem2  30349  2pthfrgrrn  30357  frgrncvvdeqlem2  30375  shincli  31437  chincli  31535  lsmsnorb  33472  quslsm  33486  coinfliprv  34640  altxpsspw  36171  mnurndlem1  44522  fourierdlem103  46453  fourierdlem104  46454  nnsum3primes4  48034  isubgr3stgrlem6  48217  grlimprclnbgrvtx  48245  grlimgrtrilem2  48248  gpgprismgr4cycllem8  48348  pgnbgreunbgr  48371