Theorem opelxp1 5706

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

Step	Hyp	Ref	Expression
1		opelxp 5700	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	simplbi 501	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2149  ⟨cop 4600   × cxp 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5407

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5178  df-xp 5670

This theorem is referenced by:  otelxp1  5709  dff3  7098  ressnop0  7153  swoord1  8729  swoord2  8730  isfin4p1  10301  canthp1lem2  10640  ciclcl  17861  txcmplem1  23769  txlm  23776  dvbsss  26032  nvvcop  30889  nvvop  30904  fldextfld1  33984  prsdm  34251  linedegen  36570  bj-opelresdm  37714  bj-idres  37729  opelopab3  38294  et-ltneverrefl  47514  natglobalincr  47522  fuco1  50021  fuco2  50023  fucoid2  50049  fucocolem2  50054  reldmlan2  50317  reldmran2  50318  lanrcl  50321  ranrcl  50322