Theorem prss 4788

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  Vcvv 3457   ⊆ wss 3906  {cpr 4593

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594

This theorem is used by:  tpss  4804  uniintsn  4952  pwssun  5555  xpsspw  5798  dffv2  6980  fiint  9289  wunex2  10734  hashfun  14487  fun2dmnop0  14554  prdsle  17532  prdsless  17533  prdsleval  17547  pwsle  17563  acsfn2  17736  joinfval  18444  joindmss  18450  meetfval  18458  meetdmss  18464  clatl  18581  ipoval  18603  ipolerval  18605  eqgfval  19267  eqgval  19268  eqg0subg  19290  gaorb  19400  pmtrrn2  19553  efgcpbllema  19847  frgpuplem  19865  isnzr2hash  20646  thlle  21876  ltbval  22223  ltbwe  22224  opsrle  22227  opsrtoslem1  22235  isphtpc  25182  axlowdimlem4  29324  structgrssvtx  29403  structgrssiedg  29404  umgredg  29517  wlk1walk  30017  wlkonl1iedg  30042  wlkdlem2  30060  3wlkdlem6  30545  frcond2  30647  frcond3  30649  nfrgr2v  30652  frgr3vlem1  30653  frgr3vlem2  30654  2pthfrgrrn  30662  frgrncvvdeqlem2  30680  shincli  31743  chincli  31841  lsmsnorb  33727  quslsm  33737  coinfliprv  34897  altxpsspw  36482  mnurndlem1  45024  fourierdlem103  46956  fourierdlem104  46957  nnsum3primes4  48586  isubgr3stgrlem6  48769  grlimprclnbgrvtx  48797  grlimgrtrilem2  48800  gpgprismgr4cycllem8  48900  pgnbgreunbgr  48923