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

Theorem opelco 5882
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 5144 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷))
2 opelco.1 . . 3 𝐴 ∈ V
3 opelco.2 . . 3 𝐵 ∈ V
42, 3brco 5881 . 2 (𝐴(𝐶𝐷)𝐵 ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
51, 4bitr3i 277 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶𝐷) ↔ ∃𝑥(𝐴𝐷𝑥𝑥𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wex 1779  wcel 2108  Vcvv 3480  cop 4632   class class class wbr 5143  ccom 5689
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-rab 3437  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-br 5144  df-opab 5206  df-co 5694
This theorem is referenced by:  dmcoss  5985  dmcosseq  5987  dmcosseqOLD  5988  cotrgOLDOLD  6129  coiun  6276  co02  6280  coi1  6282  coass  6285  fmptco  7149  dftpos4  8270  ttrcltr  9756  fmptcof2  32667  cnvco1  35759  cnvco2  35760  txpss3v  35879  dffun10  35915  xrnss3v  38373  coiun1  43665  coxp  48744
  Copyright terms: Public domain W3C validator