Theorem prss 4785

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-sn 4589  df-pr 4591

This theorem is used by:  tpss  4801  uniintsn  4949  pwssun  5552  xpsspw  5795  dffv2  6976  fiint  9284  wunex2  10729  hashfun  14481  fun2dmnop0  14548  prdsle  17521  prdsless  17522  prdsleval  17536  pwsle  17552  acsfn2  17725  joinfval  18433  joindmss  18439  meetfval  18447  meetdmss  18453  clatl  18570  ipoval  18592  ipolerval  18594  eqgfval  19250  eqgval  19251  eqg0subg  19273  gaorb  19383  pmtrrn2  19536  efgcpbllema  19830  frgpuplem  19848  isnzr2hash  20628  thlle  21858  ltbval  22205  ltbwe  22206  opsrle  22209  opsrtoslem1  22217  isphtpc  25164  axlowdimlem4  29306  structgrssvtx  29385  structgrssiedg  29386  umgredg  29499  wlk1walk  29999  wlkonl1iedg  30024  wlkdlem2  30042  3wlkdlem6  30527  frcond2  30629  frcond3  30631  nfrgr2v  30634  frgr3vlem1  30635  frgr3vlem2  30636  2pthfrgrrn  30644  frgrncvvdeqlem2  30662  shincli  31725  chincli  31823  lsmsnorb  33713  quslsm  33723  coinfliprv  34882  altxpsspw  36477  mnurndlem1  45019  fourierdlem103  46951  fourierdlem104  46952  nnsum3primes4  48581  isubgr3stgrlem6  48764  grlimprclnbgrvtx  48792  grlimgrtrilem2  48795  gpgprismgr4cycllem8  48895  pgnbgreunbgr  48918