Theorem prss 4781

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  Vcvv 3451   ⊆ wss 3899  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587

This theorem is used by:  tpss  4797  uniintsn  4945  pwssun  5543  xpsspw  5787  dffv2  6978  fiint  9311  wunex2  10816  hashfun  14575  fun2dmnop0  14642  prdsle  17626  prdsless  17627  prdsleval  17641  pwsle  17657  acsfn2  17830  joinfval  18538  joindmss  18544  meetfval  18552  meetdmss  18558  clatl  18675  ipoval  18697  ipolerval  18699  eqgfval  19381  eqgval  19382  eqg0subg  19404  gaorb  19514  pmtrrn2  19667  efgcpbllema  19961  frgpuplem  19979  isnzr2hash  20763  thlle  21996  ltbval  22345  ltbwe  22346  opsrle  22349  opsrtoslem1  22357  isphtpc  25308  axlowdimlem4  29516  structgrssvtx  29595  structgrssiedg  29596  umgredg  29709  wlk1walk  30212  wlkonl1iedg  30237  wlkdlem2  30255  3wlkdlem6  30759  frcond2  30861  frcond3  30863  nfrgr2v  30866  frgr3vlem1  30867  frgr3vlem2  30868  2pthfrgrrn  30876  frgrncvvdeqlem2  30894  shincli  31957  chincli  32055  lsmsnorb  33939  quslsm  33949  coinfliprv  35108  altxpsspw  36722  mnurndlem1  45250  fourierdlem103  47188  fourierdlem104  47189  nnsum3primes4  48855  isubgr3stgrlem6  49038  grlimprclnbgrvtx  49066  grlimgrtrilem2  49069  gpgprismgr4cycllem8  49169  pgnbgreunbgr  49192