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

Theorem opelco 5863
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 5142 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷))
2 opelco.1 . . 3 𝐴 ∈ V
3 opelco.2 . . 3 𝐵 ∈ V
42, 3brco 5862 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
51, 4bitr3i 276 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wex 1781  wcel 2106  Vcvv 3473  cop 4628   class class class wbr 5141  ccom 5673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-co 5678
This theorem is referenced by:  dmcoss  5962  dmcosseq  5964  cotrgOLDOLD  6099  coiun  6244  co02  6248  coi1  6250  coass  6253  fmptco  7111  dftpos4  8212  ttrcltr  9693  fmptcof2  31751  cnvco1  34559  cnvco2  34560  txpss3v  34680  dffun10  34716  xrnss3v  37047  coiun1  42174
  Copyright terms: Public domain W3C validator