Theorem prss 4772

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3902  {cpr 4578

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919  df-sn 4577  df-pr 4579

This theorem is referenced by:  tpss  4789  uniintsn  4935  pwssun  5508  xpsspw  5749  dffv2  6917  fiint  9211  wunex2  10629  hashfun  14344  fun2dmnop0  14411  prdsle  17366  prdsless  17367  prdsleval  17381  pwsle  17396  acsfn2  17569  joinfval  18277  joindmss  18283  meetfval  18291  meetdmss  18297  clatl  18414  ipoval  18436  ipolerval  18438  eqgfval  19089  eqgval  19090  eqg0subg  19109  gaorb  19220  pmtrrn2  19373  efgcpbllema  19667  frgpuplem  19685  isnzr2hash  20435  thlle  21635  ltbval  21979  ltbwe  21980  opsrle  21983  opsrtoslem1  21991  isphtpc  24921  axlowdimlem4  28924  structgrssvtx  29003  structgrssiedg  29004  umgredg  29117  wlk1walk  29618  wlkonl1iedg  29643  wlkdlem2  29661  3wlkdlem6  30143  frcond2  30245  frcond3  30247  nfrgr2v  30250  frgr3vlem1  30251  frgr3vlem2  30252  2pthfrgrrn  30260  frgrncvvdeqlem2  30278  shincli  31340  chincli  31438  lsmsnorb  33354  quslsm  33368  coinfliprv  34494  altxpsspw  36017  mnurndlem1  44320  fourierdlem103  46253  fourierdlem104  46254  nnsum3primes4  47825  isubgr3stgrlem6  48008  grlimprclnbgrvtx  48036  grlimgrtrilem2  48039  gpgprismgr4cycllem8  48139  pgnbgreunbgr  48162