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

Theorem opelxp1 5727
Description: The first member of an ordered pair of classes in a Cartesian product belongs to first Cartesian product argument. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opelxp1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐴𝐶)

Proof of Theorem opelxp1
StepHypRef Expression
1 opelxp 5721 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21simplbi 497 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  cop 4632   × cxp 5683
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-ral 3062  df-rex 3071  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-opab 5206  df-xp 5691
This theorem is referenced by:  otelxp1  5730  dff3  7120  ressnop0  7173  swoord1  8777  swoord2  8778  isfin4p1  10355  canthp1lem2  10693  ciclcl  17846  txcmplem1  23649  txlm  23656  dvbsss  25937  nvvcop  30613  nvvop  30628  fldextfld1  33700  prsdm  33913  linedegen  36144  bj-opelresdm  37146  bj-idres  37161  opelopab3  37725  et-ltneverrefl  46886  natglobalincr  46892  fuco1  49016  fuco2  49018  fucoid2  49044  fucocolem2  49049
  Copyright terms: Public domain W3C validator