Theorem prss 4778

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585

This theorem is referenced by:  tpss  4795  uniintsn  4942  pwssun  5524  xpsspw  5766  dffv2  6937  fiint  9239  wunex2  10661  hashfun  14372  fun2dmnop0  14439  prdsle  17394  prdsless  17395  prdsleval  17409  pwsle  17425  acsfn2  17598  joinfval  18306  joindmss  18312  meetfval  18320  meetdmss  18326  clatl  18443  ipoval  18465  ipolerval  18467  eqgfval  19117  eqgval  19118  eqg0subg  19137  gaorb  19248  pmtrrn2  19401  efgcpbllema  19695  frgpuplem  19713  isnzr2hash  20464  thlle  21664  ltbval  22010  ltbwe  22011  opsrle  22014  opsrtoslem1  22022  isphtpc  24961  axlowdimlem4  29030  structgrssvtx  29109  structgrssiedg  29110  umgredg  29223  wlk1walk  29724  wlkonl1iedg  29749  wlkdlem2  29767  3wlkdlem6  30252  frcond2  30354  frcond3  30356  nfrgr2v  30359  frgr3vlem1  30360  frgr3vlem2  30361  2pthfrgrrn  30369  frgrncvvdeqlem2  30387  shincli  31449  chincli  31547  lsmsnorb  33483  quslsm  33497  coinfliprv  34660  altxpsspw  36190  mnurndlem1  44634  fourierdlem103  46564  fourierdlem104  46565  nnsum3primes4  48145  isubgr3stgrlem6  48328  grlimprclnbgrvtx  48356  grlimgrtrilem2  48359  gpgprismgr4cycllem8  48459  pgnbgreunbgr  48482