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

Theorem prss 4779
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 4778 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
41, 2, 3mp2an 691 1 ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wcel 2107  Vcvv 3444  wss 3909  {cpr 4587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-un 3914  df-in 3916  df-ss 3926  df-sn 4586  df-pr 4588
This theorem is referenced by:  tpss  4794  uniintsn  4947  pwssun  5526  xpsspw  5762  dffv2  6932  fiint  9202  wunex2  10608  hashfun  14265  fun2dmnop0  14321  prdsle  17279  prdsless  17280  prdsleval  17294  pwsle  17309  acsfn2  17478  joinfval  18197  joindmss  18203  meetfval  18211  meetdmss  18217  clatl  18332  ipoval  18354  ipolerval  18356  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  27680  structgrssvtx  27761  structgrssiedg  27762  umgredg  27875  wlk1walk  28373  wlkonl1iedg  28399  wlkdlem2  28417  3wlkdlem6  28895  frcond2  28997  frcond3  28999  nfrgr2v  29002  frgr3vlem1  29003  frgr3vlem2  29004  2pthfrgrrn  29012  frgrncvvdeqlem2  29030  shincli  30090  chincli  30188  lsmsnorb  31953  quslsm  31967  coinfliprv  32843  altxpsspw  34448  mnurndlem1  42294  fourierdlem103  44172  fourierdlem104  44173  nnsum3primes4  45698
  Copyright terms: Public domain W3C validator