Theorem prss 4787

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3906  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593

This theorem is referenced by:  tpss  4803  uniintsn  4951  pwssun  5555  xpsspw  5798  dffv2  6978  fiint  9287  wunex2  10724  hashfun  14476  fun2dmnop0  14543  prdsle  17516  prdsless  17517  prdsleval  17531  pwsle  17547  acsfn2  17720  joinfval  18428  joindmss  18434  meetfval  18442  meetdmss  18448  clatl  18565  ipoval  18587  ipolerval  18589  eqgfval  19245  eqgval  19246  eqg0subg  19268  gaorb  19378  pmtrrn2  19531  efgcpbllema  19825  frgpuplem  19843  isnzr2hash  20604  thlle  21828  ltbval  22175  ltbwe  22176  opsrle  22179  opsrtoslem1  22187  isphtpc  25134  axlowdimlem4  29276  structgrssvtx  29355  structgrssiedg  29356  umgredg  29469  wlk1walk  29969  wlkonl1iedg  29994  wlkdlem2  30012  3wlkdlem6  30497  frcond2  30599  frcond3  30601  nfrgr2v  30604  frgr3vlem1  30605  frgr3vlem2  30606  2pthfrgrrn  30614  frgrncvvdeqlem2  30632  shincli  31695  chincli  31793  lsmsnorb  33685  quslsm  33695  coinfliprv  34854  altxpsspw  36450  mnurndlem1  44974  fourierdlem103  46906  fourierdlem104  46907  nnsum3primes4  48536  isubgr3stgrlem6  48719  grlimprclnbgrvtx  48747  grlimgrtrilem2  48750  gpgprismgr4cycllem8  48850  pgnbgreunbgr  48873