Theorem prss 4290

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

Syntax hints:   ↔ wb 194   ∧ wa 382   ∈ wcel 1976  Vcvv 3172   ⊆ wss 3539  {cpr 4126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553  df-sn 4125  df-pr 4127

This theorem is referenced by:  tpss  4303  uniintsn  4443  pwssun  4934  xpsspw  5145  dffv2  6166  fpr2g  6358  fiint  8100  wunex2  9417  hashfun  13039  prdsle  15894  prdsless  15895  prdsleval  15909  pwsle  15924  acsfn2  16096  joinfval  16773  joindmss  16779  meetfval  16787  meetdmss  16793  clatl  16888  ipoval  16926  ipolerval  16928  eqgfval  17414  eqgval  17415  gaorb  17512  pmtrrn2  17652  efgcpbllema  17939  frgpuplem  17957  drngnidl  18999  drnglpir  19023  isnzr2hash  19034  ltbval  19241  ltbwe  19242  opsrle  19245  opsrtoslem1  19254  thlle  19808  isphtpc  22549  axlowdimlem4  25571  usgrarnedg  25707  cusgrarn  25782  frgraun  26317  frisusgranb  26318  frgra2v  26320  frgra3vlem1  26321  frgra3vlem2  26322  2pthfrgrarn  26330  frgrancvvdeqlem3  26353  shincli  27439  chincli  27537  coinfliprv  29705  altxpsspw  31088  fourierdlem103  38926  fourierdlem104  38927  nnsum3primes4  40029  fun2dmnop0  40174  structgrssvtxlem  40278  structgrssvtx  40279  structgrssiedg  40280  umgredg  40393  1wlk1walk  40865  wlkOnl1iedg  40895  1wlkdlem2  40914  31wlkdlem6  41354  frcond2  41461  frcond3  41462  nfrgr2v  41464  frgr3vlem1  41465  frgr3vlem2  41466  2pthfrgrrn  41474  frgrncvvdeqlem3  41493