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

Theorem otex 5466
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 4638 . 2 𝐴, 𝐵, 𝐶⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶
2 opex 5465 . 2 ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ V
31, 2eqeltri 2830 1 𝐴, 𝐵, 𝐶⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3475  cop 4635  cotp 4637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-ot 4638
This theorem is referenced by:  euotd  5514  ralxp3f  8123  xpord3lem  8135  xpord3pred  8138  splval  14701  splcl  14702  idaval  18008  idaf  18013  eldmcoa  18015  coaval  18018  mamufval  21887  msrval  34529  msrf  34533  mapdhval  40595  mndtcco  47711
  Copyright terms: Public domain W3C validator