Theorem prss 4825

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2106  Vcvv 3478   ⊆ wss 3963  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-sn 4632  df-pr 4634

This theorem is referenced by:  tpss  4842  uniintsn  4990  pwssun  5580  xpsspw  5822  dffv2  7004  fiint  9364  fiintOLD  9365  wunex2  10776  hashfun  14473  fun2dmnop0  14540  prdsle  17509  prdsless  17510  prdsleval  17524  pwsle  17539  acsfn2  17708  joinfval  18431  joindmss  18437  meetfval  18445  meetdmss  18451  clatl  18566  ipoval  18588  ipolerval  18590  eqgfval  19207  eqgval  19208  eqg0subg  19227  gaorb  19338  pmtrrn2  19493  efgcpbllema  19787  frgpuplem  19805  isnzr2hash  20536  thlle  21734  thlleOLD  21735  ltbval  22079  ltbwe  22080  opsrle  22083  opsrtoslem1  22097  isphtpc  25040  axlowdimlem4  28975  structgrssvtx  29056  structgrssiedg  29057  umgredg  29170  wlk1walk  29672  wlkonl1iedg  29698  wlkdlem2  29716  3wlkdlem6  30194  frcond2  30296  frcond3  30298  nfrgr2v  30301  frgr3vlem1  30302  frgr3vlem2  30303  2pthfrgrrn  30311  frgrncvvdeqlem2  30329  shincli  31391  chincli  31489  lsmsnorb  33399  quslsm  33413  coinfliprv  34464  altxpsspw  35959  mnurndlem1  44277  fourierdlem103  46165  fourierdlem104  46166  nnsum3primes4  47713  isubgr3stgrlem6  47874  grlimgrtrilem2  47898