Theorem opelxp1 5703

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ⟨cop 4595   × cxp 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174  df-xp 5667

This theorem is used by:  otelxp1  5706  dff3  7095  ressnop0  7150  swoord1  8723  swoord2  8724  isfin4p1  10303  canthp1lem2  10642  ciclcl  17863  txcmplem1  23807  txlm  23814  dvbsss  26070  nvvcop  30955  nvvop  30970  fldextfld1  34046  prsdm  34313  linedegen  36643  bj-opelresdm  37817  bj-idres  37832  opelopab3  38397  et-ltneverrefl  47613  natglobalincr  47621  fuco1  50127  fuco2  50129  fucoid2  50155  fucocolem2  50160  reldmlan2  50423  reldmran2  50424  lanrcl  50427  ranrcl  50428