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

Theorem otex 5470
Description: An ordered triple of classes is a set. (Contributed by NM, 3-Apr-2015.)
Assertion
Ref Expression
otex 𝐴, 𝐵, 𝐶⟩ ∈ V

Proof of Theorem otex
StepHypRef Expression
1 df-ot 4635 . 2 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
2 opex 5469 . 2 ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ V
31, 2eqeltri 2837 1 𝐴, 𝐵, 𝐶⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2108  Vcvv 3480  cop 4632  cotp 4634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-ot 4635
This theorem is referenced by:  euotd  5518  ralxp3f  8162  xpord3lem  8174  xpord3pred  8177  splval  14789  splcl  14790  idaval  18103  idaf  18108  eldmcoa  18110  coaval  18113  mamufval  22396  msrval  35543  msrf  35547  mapdhval  41726  mndtcco  49182
  Copyright terms: Public domain W3C validator