Theorem prss 4775

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3902  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919  df-sn 4580  df-pr 4582

This theorem is referenced by:  tpss  4792  uniintsn  4940  pwssun  5535  xpsspw  5778  dffv2  6956  fiint  9264  wunex2  10689  hashfun  14443  fun2dmnop0  14510  prdsle  17481  prdsless  17482  prdsleval  17496  pwsle  17512  acsfn2  17685  joinfval  18393  joindmss  18399  meetfval  18407  meetdmss  18413  clatl  18530  ipoval  18552  ipolerval  18554  eqgfval  19207  eqgval  19208  eqg0subg  19227  gaorb  19337  pmtrrn2  19490  efgcpbllema  19784  frgpuplem  19802  isnzr2hash  20555  thlle  21736  ltbval  22083  ltbwe  22084  opsrle  22087  opsrtoslem1  22095  isphtpc  25043  axlowdimlem4  29102  structgrssvtx  29181  structgrssiedg  29182  umgredg  29295  wlk1walk  29795  wlkonl1iedg  29820  wlkdlem2  29838  3wlkdlem6  30323  frcond2  30425  frcond3  30427  nfrgr2v  30430  frgr3vlem1  30431  frgr3vlem2  30432  2pthfrgrrn  30440  frgrncvvdeqlem2  30458  shincli  31521  chincli  31619  lsmsnorb  33537  quslsm  33551  coinfliprv  34740  altxpsspw  36287  mnurndlem1  44817  fourierdlem103  46743  fourierdlem104  46744  nnsum3primes4  48370  isubgr3stgrlem6  48553  grlimprclnbgrvtx  48581  grlimgrtrilem2  48584  gpgprismgr4cycllem8  48684  pgnbgreunbgr  48707