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

Theorem prssi 4292
Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.)
Assertion
Ref Expression
prssi ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Proof of Theorem prssi
StepHypRef Expression
1 prssg 4289 . 2 ((𝐴𝐶𝐵𝐶) → ((𝐴𝐶𝐵𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
21ibi 254 1 ((𝐴𝐶𝐵𝐶) → {𝐴, 𝐵} ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  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:  prssd  4293  tpssi  4304  prelpwi  4835  fr2nr  5005  f1prex  6416  fveqf1o  6434  fr3nr  6848  ordunel  6896  1sdom  8025  en2eqpr  8690  en2eleq  8691  r0weon  8695  dfac2  8813  wuncval2  9425  tskpr  9448  m1expcl2  12701  m1expcl  12702  wrdlen2i  13482  gcdcllem3  15009  lcmfpr  15126  1idssfct  15179  mreincl  16030  mrcun  16053  acsfn2  16095  joinval2  16780  meetval2  16794  ipole  16929  pmtrprfv  17644  pmtrprfv3  17645  symggen  17661  pmtr3ncomlem1  17664  pmtr3ncom  17666  psgnunilem1  17684  subrgin  18574  lssincl  18734  lspprcl  18747  lsptpcl  18748  lspprid1  18766  lspvadd  18865  lsppratlem2  18917  lsppratlem4  18919  cnmsgnbas  19690  cnmsgngrp  19691  psgninv  19694  zrhpsgnmhm  19696  mdetralt  20180  mdetunilem7  20190  unopn  20480  pptbas  20569  incld  20604  indiscld  20652  leordtval2  20773  iscon2  20974  xpsdsval  21943  ovolioo  23087  i1f1  23207  itgioo  23332  aannenlem2  23832  wilthlem2  24539  perfectlem2  24699  umgraex  25645  umgra1  25648  uslgra1  25694  constr1trl  25911  constr3trllem3  25973  nbhashuvtx1  26235  eupath2  26300  umgrabi  26303  konigsberg  26307  frgra3vlem2  26321  4cycl2v2nb  26336  sshjval3  27390  psgnid  28971  pmtrto1cl  28973  mdetpmtr1  29010  mdetpmtr12  29012  pr01ssre  29200  esumsnf  29246  prsiga  29314  difelsiga  29316  inelpisys  29337  measssd  29398  carsgsigalem  29497  carsgclctun  29503  pmeasmono  29506  eulerpartlemgs2  29562  eulerpartlemn  29563  probun  29601  signswch  29757  signsvfn  29778  signlem0  29783  kur14lem1  30235  fprb  30709  ssoninhaus  31410  poimirlem15  32377  inidl  32782  pmapmeet  33860  diameetN  35146  dihmeetcN  35392  dihmeet  35433  dvh4dimlem  35533  dvhdimlem  35534  dvh4dimN  35537  dvh3dim3N  35539  lcfrlem23  35655  lcfrlem25  35657  lcfrlem35  35667  mapdindp2  35811  lspindp5  35860  brfvrcld  36785  corclrcl  36801  corcltrcl  36833  ibliooicc  38646  fourierdlem51  38833  fourierdlem64  38846  fourierdlem102  38884  fourierdlem114  38896  sge0sn  39055  ovnsubadd2lem  39318  perfectALTVlem2  39949  nnsum3primesgbe  39992  upgrbi  40300  umgrbi  40307  frgr3vlem2  41425  4cycl2v2nb-av  41440  mapprop  41898  zlmodzxzel  41907  zlmodzxzldeplem1  42064
  Copyright terms: Public domain W3C validator