Theorem opelxp2 5674

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

Step	Hyp	Ref	Expression
1		opelxp 5667	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	simprbi 497	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐵 ∈ 𝐷)

Syntax hints:   → wi 4   ∈ wcel 2114  ⟨cop 4573   × cxp 5629

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-xp 5637

This theorem is referenced by:  dff4  7053  eceqoveq  8769  axdc4lem  10377  canthp1lem2  10576  cicrcl  17770  txcmplem1  23606  txlm  23613  brcgr  28969  nvex  30682  fldextfld2  33792  prsrn  34059  pprodss4v  36064  poimirlem27  37968  natglobalincr  47307  fuco1  49796  fuco2  49798  fucoid2  49824  fucocolem2  49829  reldmlan2  50092  reldmran2  50093  lanrcl  50096  ranrcl  50097