Theorem prssi 4754

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   ⊆ wss 3936  {cpr 4569

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-sn 4568  df-pr 4570

This theorem is referenced by:  prssd  4755  tpssi  4769  fr2nr  5533  fprb  6956  ordunel  7542  1sdom  8721  dfac2b  9556  tskpr  10192  m1expcl2  13452  m1expcl  13453  wrdlen2i  14304  gcdcllem3  15850  lcmfpr  15971  mreincl  16870  acsfn2  16934  ipole  17768  pmtr3ncom  18603  subrgin  19558  lssincl  19737  lspvadd  19868  cnmsgnbas  20722  cnmsgngrp  20723  psgninv  20726  zrhpsgnmhm  20728  mdetunilem7  21227  unopn  21511  incld  21651  indiscld  21699  leordtval2  21820  ovolioo  24169  i1f1  24291  aannenlem2  24918  upgrbi  26878  umgrbi  26886  frgr3vlem2  28053  4cycl2v2nb  28068  sshjval3  29131  pr01ssre  30540  psgnid  30739  pmtrto1cl  30741  cnmsgn0g  30788  altgnsg  30791  mdetpmtr1  31088  mdetpmtr12  31090  esumsnf  31323  prsiga  31390  difelsiga  31392  inelpisys  31413  measssd  31474  carsgsigalem  31573  carsgclctun  31579  pmeasmono  31582  eulerpartlemgs2  31638  eulerpartlemn  31639  probun  31677  signswch  31831  signsvfn  31852  signlem0  31857  breprexpnat  31905  kur14lem1  32453  ssoninhaus  33796  poimirlem15  34922  inidl  35323  pmapmeet  36924  diameetN  38207  dihmeetcN  38453  dihmeet  38494  dvh4dimlem  38594  dvhdimlem  38595  dvh4dimN  38598  dvh3dim3N  38600  lcfrlem23  38716  lcfrlem25  38718  lcfrlem35  38728  mapdindp2  38872  lspindp5  38921  brfvrcld  40085  corclrcl  40101  corcltrcl  40133  ibliooicc  42305  fourierdlem51  42491  fourierdlem64  42504  fourierdlem102  42542  fourierdlem114  42554  sge0sn  42710  ovnsubadd2lem  42976  sprvalpw  43691  prprvalpw  43726  perfectALTVlem2  43936  nnsum3primesgbe  44006  mapprop  44443  zlmodzxzel  44452  zlmodzxzldeplem1  44604  prelrrx2  44749  line2x  44790  line2y  44791  onsetreclem2  44857