Theorem prssi 4770

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 4768	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶))
2	1	ibi 267	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3897  {cpr 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-sn 4574  df-pr 4576

This theorem is referenced by:  prssd  4771  tpssi  4787  fr2nr  5591  fprb  7128  f1ofvswap  7240  ordunel  7757  rex2dom  9137  dfac2b  10022  tskpr  10661  m1expcl2  13992  m1expcl  13993  wrdlen2i  14849  gcdcllem3  16412  lcmfpr  16538  mreincl  17501  acsfn2  17569  ipole  18440  pmtr3ncom  19387  subrngin  20476  subrgin  20511  lssincl  20898  lspvadd  21030  cnmsgnbas  21515  cnmsgngrp  21516  psgninv  21519  zrhpsgnmhm  21521  mdetunilem7  22533  unopn  22818  incld  22958  indiscld  23006  leordtval2  23127  ovolioo  25496  i1f1  25618  aannenlem2  26264  upgrbi  29071  umgrbi  29079  frgr3vlem2  30254  4cycl2v2nb  30269  sshjval3  31334  pr01ssre  32807  psgnid  33066  pmtrto1cl  33068  cnmsgn0g  33115  altgnsg  33118  constrsscn  33753  constrextdg2  33762  mdetpmtr1  33836  mdetpmtr12  33838  esumsnf  34077  prsiga  34144  difelsiga  34146  measssd  34228  carsgsigalem  34328  carsgclctun  34334  pmeasmono  34337  eulerpartlemgs2  34393  eulerpartlemn  34394  probun  34432  signswch  34574  signsvfn  34595  signlem0  34600  breprexpnat  34647  kur14lem1  35250  ssoninhaus  36492  poimirlem15  37685  inidl  38080  pmapmeet  39882  diameetN  41165  dihmeetcN  41411  dihmeet  41452  dvh4dimlem  41552  dvhdimlem  41553  dvh4dimN  41556  dvh3dim3N  41558  lcfrlem23  41674  lcfrlem25  41676  lcfrlem35  41686  mapdindp2  41830  lspindp5  41879  brfvrcld  43794  corclrcl  43810  corcltrcl  43842  ibliooicc  46079  fourierdlem51  46265  fourierdlem64  46278  fourierdlem102  46316  fourierdlem114  46328  sge0sn  46487  ovnsubadd2lem  46753  sprvalpw  47590  prprvalpw  47625  perfectALTVlem2  47832  nnsum3primesgbe  47902  clnbgredg  47950  uhgrimprop  48002  isuspgrimlem  48005  isubgr3stgrlem7  48082  usgrexmpl1lem  48131  usgrexmpl2lem  48136  usgrexmpl2nb1  48142  usgrexmpl2nb2  48143  usgrexmpl2nb4  48145  usgrexmpl2nb5  48146  pgnbgreunbgr  48235  fprmappr  48455  zlmodzxzel  48465  zlmodzxzldeplem1  48611  2arymaptfo  48765  prelrrx2  48824  line2x  48865  line2y  48866  onsetreclem2  49817