MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prss Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 prss.1 . 2 𝐴 ∈ V
2 prss.2 . 2 𝐵 ∈ V
3 prssg 4289 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
41, 2, 3mp2an 703 1 ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator