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

Theorem opelxp2 5728
Description: The second member of an ordered pair of classes in a Cartesian product belongs to second Cartesian product argument. (Contributed by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opelxp2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐵𝐷)

Proof of Theorem opelxp2
StepHypRef Expression
1 opelxp 5721 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
21simprbi 496 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:  dff4  7121  eceqoveq  8862  axdc4lem  10495  canthp1lem2  10693  cicrcl  17847  txcmplem1  23649  txlm  23656  brcgr  28915  nvex  30630  fldextfld2  33701  prsrn  33914  pprodss4v  35885  poimirlem27  37654  natglobalincr  46892  fuco1  49016  fuco2  49018  fucoid2  49044  fucocolem2  49049
  Copyright terms: Public domain W3C validator