Theorem prss 4291

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

Syntax hints:   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554  df-sn 4126  df-pr 4128

This theorem is referenced by:  tpss  4308  uniintsn  4449  pwssun  4944  xpsspw  5156  dffv2  6181  fpr2g  6380  fiint  8122  wunex2  9439  hashfun  13084  fun2dmnop0  13131  prdsle  15945  prdsless  15946  prdsleval  15960  pwsle  15975  acsfn2  16147  joinfval  16824  joindmss  16830  meetfval  16838  meetdmss  16844  clatl  16939  ipoval  16977  ipolerval  16979  eqgfval  17465  eqgval  17466  gaorb  17563  pmtrrn2  17703  efgcpbllema  17990  frgpuplem  18008  drngnidl  19050  drnglpir  19074  isnzr2hash  19085  ltbval  19292  ltbwe  19293  opsrle  19296  opsrtoslem1  19305  thlle  19860  isphtpc  22601  axlowdimlem4  25625  structgrssvtxlem  25700  structgrssvtx  25701  structgrssiedg  25702  umgredg  25812  usgrarnedg  25913  cusgrarn  25988  frgraun  26523  frisusgranb  26524  frgra2v  26526  frgra3vlem1  26527  frgra3vlem2  26528  2pthfrgrarn  26536  frgrancvvdeqlem3  26559  shincli  27605  chincli  27703  coinfliprv  29871  altxpsspw  31254  fourierdlem103  39102  fourierdlem104  39103  nnsum3primes4  40204  1wlk1walk  40843  wlkOnl1iedg  40873  1wlkdlem2  40892  31wlkdlem6  41332  frcond2  41439  frcond3  41440  nfrgr2v  41442  frgr3vlem1  41443  frgr3vlem2  41444  2pthfrgrrn  41452  frgrncvvdeqlem3  41471