Theorem prss 4787

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917  {cpr 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-sn 4593  df-pr 4595

This theorem is referenced by:  tpss  4804  uniintsn  4952  pwssun  5533  xpsspw  5775  dffv2  6959  fiint  9284  fiintOLD  9285  wunex2  10698  hashfun  14409  fun2dmnop0  14476  prdsle  17432  prdsless  17433  prdsleval  17447  pwsle  17462  acsfn2  17631  joinfval  18339  joindmss  18345  meetfval  18353  meetdmss  18359  clatl  18474  ipoval  18496  ipolerval  18498  eqgfval  19115  eqgval  19116  eqg0subg  19135  gaorb  19246  pmtrrn2  19397  efgcpbllema  19691  frgpuplem  19709  isnzr2hash  20435  thlle  21613  ltbval  21957  ltbwe  21958  opsrle  21961  opsrtoslem1  21969  isphtpc  24900  axlowdimlem4  28879  structgrssvtx  28958  structgrssiedg  28959  umgredg  29072  wlk1walk  29574  wlkonl1iedg  29600  wlkdlem2  29618  3wlkdlem6  30101  frcond2  30203  frcond3  30205  nfrgr2v  30208  frgr3vlem1  30209  frgr3vlem2  30210  2pthfrgrrn  30218  frgrncvvdeqlem2  30236  shincli  31298  chincli  31396  lsmsnorb  33369  quslsm  33383  coinfliprv  34481  altxpsspw  35972  mnurndlem1  44277  fourierdlem103  46214  fourierdlem104  46215  nnsum3primes4  47793  isubgr3stgrlem6  47974  grlimgrtrilem2  47998  gpgprismgr4cycllem8  48096  pgnbgreunbgr  48119