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

Theorem prss 4496
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 4495 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
41, 2, 3mp2an 710 1 ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wcel 2139  Vcvv 3340  wss 3715  {cpr 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-in 3722  df-ss 3729  df-sn 4322  df-pr 4324
This theorem is referenced by:  tpss  4513  uniintsn  4666  pwssun  5170  xpsspw  5389  dffv2  6434  fpr2g  6640  fiint  8404  wunex2  9772  hashfun  13436  fun2dmnop0  13488  prdsle  16344  prdsless  16345  prdsleval  16359  pwsle  16374  acsfn2  16545  joinfval  17222  joindmss  17228  meetfval  17236  meetdmss  17242  clatl  17337  ipoval  17375  ipolerval  17377  eqgfval  17863  eqgval  17864  gaorb  17960  pmtrrn2  18100  efgcpbllema  18387  frgpuplem  18405  drngnidl  19451  drnglpir  19475  isnzr2hash  19486  ltbval  19693  ltbwe  19694  opsrle  19697  opsrtoslem1  19706  thlle  20263  isphtpc  23014  axlowdimlem4  26045  structgrssvtx  26133  structgrssiedg  26134  structgrssvtxlemOLD  26135  structgrssvtxOLD  26136  structgrssiedgOLD  26137  umgredg  26253  wlk1walk  26766  wlkonl1iedg  26792  wlkdlem2  26811  3wlkdlem6  27338  frcond2  27442  frcond3  27444  nfrgr2v  27447  frgr3vlem1  27448  frgr3vlem2  27449  2pthfrgrrn  27457  frgrncvvdeqlem2  27475  shincli  28551  chincli  28649  coinfliprv  30874  altxpsspw  32411  fourierdlem103  40947  fourierdlem104  40948  nnsum3primes4  42204
  Copyright terms: Public domain W3C validator