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

Theorem opelco 5872
Description: Ordered pair membership in a composition. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 24-Feb-2015.)
Hypotheses
Ref Expression
opelco.1 𝐴 ∈ V
opelco.2 𝐵 ∈ V
Assertion
Ref Expression
opelco (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑥,𝐷

Proof of Theorem opelco
StepHypRef Expression
1 df-br 5150 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷))
2 opelco.1 . . 3 𝐴 ∈ V
3 opelco.2 . . 3 𝐵 ∈ V
42, 3brco 5871 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
51, 4bitr3i 277 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782  wcel 2107  Vcvv 3475  cop 4635   class class class wbr 5149  ccom 5681
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-rab 3434  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-br 5150  df-opab 5212  df-co 5686
This theorem is referenced by:  dmcoss  5971  dmcosseq  5973  cotrgOLDOLD  6111  coiun  6256  co02  6260  coi1  6262  coass  6265  fmptco  7127  dftpos4  8230  ttrcltr  9711  fmptcof2  31882  cnvco1  34729  cnvco2  34730  txpss3v  34850  dffun10  34886  xrnss3v  37242  coiun1  42403
  Copyright terms: Public domain W3C validator