Theorem opelxp1 5691

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 5685	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
2	1	simplbi 500	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2144  ⟨cop 4590   × cxp 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5165  df-xp 5655

This theorem is referenced by:  otelxp1  5694  dff3  7083  ressnop0  7138  swoord1  8713  swoord2  8714  isfin4p1  10274  canthp1lem2  10613  ciclcl  17837  txcmplem1  23703  txlm  23710  dvbsss  25966  nvvcop  30799  nvvop  30814  fldextfld1  33946  prsdm  34213  linedegen  36498  bj-opelresdm  37642  bj-idres  37657  opelopab3  38222  et-ltneverrefl  47450  natglobalincr  47458  fuco1  49947  fuco2  49949  fucoid2  49975  fucocolem2  49980  reldmlan2  50243  reldmran2  50244  lanrcl  50247  ranrcl  50248