Theorem prss 4773

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898  {cpr 4579

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915  df-sn 4578  df-pr 4580

This theorem is referenced by:  tpss  4790  uniintsn  4937  pwssun  5513  xpsspw  5755  dffv2  6925  fiint  9220  wunex2  10638  hashfun  14348  fun2dmnop0  14415  prdsle  17370  prdsless  17371  prdsleval  17385  pwsle  17400  acsfn2  17573  joinfval  18281  joindmss  18287  meetfval  18295  meetdmss  18301  clatl  18418  ipoval  18440  ipolerval  18442  eqgfval  19092  eqgval  19093  eqg0subg  19112  gaorb  19223  pmtrrn2  19376  efgcpbllema  19670  frgpuplem  19688  isnzr2hash  20438  thlle  21638  ltbval  21981  ltbwe  21982  opsrle  21985  opsrtoslem1  21993  isphtpc  24923  axlowdimlem4  28927  structgrssvtx  29006  structgrssiedg  29007  umgredg  29120  wlk1walk  29621  wlkonl1iedg  29646  wlkdlem2  29664  3wlkdlem6  30149  frcond2  30251  frcond3  30253  nfrgr2v  30256  frgr3vlem1  30257  frgr3vlem2  30258  2pthfrgrrn  30266  frgrncvvdeqlem2  30284  shincli  31346  chincli  31444  lsmsnorb  33365  quslsm  33379  coinfliprv  34519  altxpsspw  36044  mnurndlem1  44401  fourierdlem103  46334  fourierdlem104  46335  nnsum3primes4  47915  isubgr3stgrlem6  48098  grlimprclnbgrvtx  48126  grlimgrtrilem2  48129  gpgprismgr4cycllem8  48229  pgnbgreunbgr  48252