Theorem prssi 4487

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

Step	Hyp	Ref	Expression
1		prssg 4485	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
2	1	ibi 256	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 2145   ⊆ wss 3723  {cpr 4318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-in 3730  df-ss 3737  df-sn 4317  df-pr 4319

This theorem is referenced by:  prssd  4488  tpssi  4502  fr2nr  5227  f1prex  6681  fveqf1o  6699  fr3nr  7126  ordunel  7174  1sdom  8319  en2eqpr  9030  en2eleq  9031  r0weon  9035  dfac2b  9153  dfac2OLD  9155  wuncval2  9771  tskpr  9794  m1expcl2  13085  m1expcl  13086  wrdlen2i  13892  gcdcllem3  15427  lcmfpr  15544  1idssfct  15596  mreincl  16463  mrcun  16486  acsfn2  16527  joinval2  17213  meetval2  17227  ipole  17362  pmtrprfv  18076  pmtrprfv3  18077  symggen  18093  pmtr3ncomlem1  18096  pmtr3ncom  18098  psgnunilem1  18116  subrgin  19009  lssincl  19174  lspprcl  19187  lsptpcl  19188  lspprid1  19206  lspvadd  19305  lsppratlem2  19359  lsppratlem4  19361  cnmsgnbas  20135  cnmsgngrp  20136  psgninv  20139  zrhpsgnmhm  20141  mdetralt  20628  mdetunilem7  20638  unopn  20924  pptbas  21029  incld  21064  indiscld  21112  leordtval2  21233  isconn2  21434  xpsdsval  22402  ovolioo  23552  i1f1  23673  itgioo  23798  aannenlem2  24300  wilthlem2  25012  perfectlem2  25172  upgrbi  26205  umgrbi  26213  frgr3vlem2  27452  4cycl2v2nb  27467  sshjval3  28549  pr01ssre  29906  psgnid  30183  pmtrto1cl  30185  mdetpmtr1  30225  mdetpmtr12  30227  esumsnf  30462  prsiga  30530  difelsiga  30532  inelpisys  30553  measssd  30614  carsgsigalem  30713  carsgclctun  30719  pmeasmono  30722  eulerpartlemgs2  30778  eulerpartlemn  30779  probun  30817  signswch  30974  signsvfn  30995  signlem0  31000  breprexpnat  31048  kur14lem1  31522  fprb  32003  ssoninhaus  32780  poimirlem15  33753  inidl  34157  pmapmeet  35578  diameetN  36863  dihmeetcN  37109  dihmeet  37150  dvh4dimlem  37250  dvhdimlem  37251  dvh4dimN  37254  dvh3dim3N  37256  lcfrlem23  37372  lcfrlem25  37374  lcfrlem35  37384  mapdindp2  37528  lspindp5  37577  brfvrcld  38506  corclrcl  38522  corcltrcl  38554  ibliooicc  40701  fourierdlem51  40888  fourierdlem64  40901  fourierdlem102  40939  fourierdlem114  40951  sge0sn  41110  ovnsubadd2lem  41376  perfectALTVlem2  42156  nnsum3primesgbe  42205  sprvalpw  42255  mapprop  42649  zlmodzxzel  42658  zlmodzxzldeplem1  42814  onsetreclem2  42977