Theorem prss 4764

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  {cpr 4570

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 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571

This theorem is referenced by:  tpss  4781  uniintsn  4928  pwssun  5516  xpsspw  5758  dffv2  6929  fiint  9230  wunex2  10652  hashfun  14390  fun2dmnop0  14457  prdsle  17416  prdsless  17417  prdsleval  17431  pwsle  17447  acsfn2  17620  joinfval  18328  joindmss  18334  meetfval  18342  meetdmss  18348  clatl  18465  ipoval  18487  ipolerval  18489  eqgfval  19142  eqgval  19143  eqg0subg  19162  gaorb  19273  pmtrrn2  19426  efgcpbllema  19720  frgpuplem  19738  isnzr2hash  20487  thlle  21687  ltbval  22031  ltbwe  22032  opsrle  22035  opsrtoslem1  22043  isphtpc  24971  axlowdimlem4  29028  structgrssvtx  29107  structgrssiedg  29108  umgredg  29221  wlk1walk  29722  wlkonl1iedg  29747  wlkdlem2  29765  3wlkdlem6  30250  frcond2  30352  frcond3  30354  nfrgr2v  30357  frgr3vlem1  30358  frgr3vlem2  30359  2pthfrgrrn  30367  frgrncvvdeqlem2  30385  shincli  31448  chincli  31546  lsmsnorb  33466  quslsm  33480  coinfliprv  34643  altxpsspw  36175  mnurndlem1  44726  fourierdlem103  46655  fourierdlem104  46656  nnsum3primes4  48276  isubgr3stgrlem6  48459  grlimprclnbgrvtx  48487  grlimgrtrilem2  48490  gpgprismgr4cycllem8  48590  pgnbgreunbgr  48613