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

Theorem prss 4778
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 4777 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
41, 2, 3mp2an 690 1 ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wcel 2106  Vcvv 3443  wss 3908  {cpr 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-un 3913  df-in 3915  df-ss 3925  df-sn 4585  df-pr 4587
This theorem is referenced by:  tpss  4793  uniintsn  4946  pwssun  5525  xpsspw  5761  dffv2  6931  fiint  9201  wunex2  10607  hashfun  14264  fun2dmnop0  14320  prdsle  17278  prdsless  17279  prdsleval  17293  pwsle  17308  acsfn2  17477  joinfval  18196  joindmss  18202  meetfval  18210  meetdmss  18216  clatl  18331  ipoval  18353  ipolerval  18355  eqgfval  18910  eqgval  18911  gaorb  19019  pmtrrn2  19174  efgcpbllema  19465  frgpuplem  19483  isnzr2hash  20657  thlle  21025  thlleOLD  21026  ltbval  21366  ltbwe  21367  opsrle  21370  opsrtoslem1  21384  isphtpc  24279  axlowdimlem4  27692  structgrssvtx  27773  structgrssiedg  27774  umgredg  27887  wlk1walk  28385  wlkonl1iedg  28411  wlkdlem2  28429  3wlkdlem6  28907  frcond2  29009  frcond3  29011  nfrgr2v  29014  frgr3vlem1  29015  frgr3vlem2  29016  2pthfrgrrn  29024  frgrncvvdeqlem2  29042  shincli  30102  chincli  30200  lsmsnorb  31965  quslsm  31979  coinfliprv  32855  altxpsspw  34457  mnurndlem1  42325  fourierdlem103  44203  fourierdlem104  44204  nnsum3primes4  45729
  Copyright terms: Public domain W3C validator