Theorem opelxp1 5692

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ⟨cop 4589   × cxp 5648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-opab 5167  df-xp 5656

This theorem is used by:  otelxp1  5695  dff3  7100  ressnop0  7157  swoord1  8750  swoord2  8751  isfin4p1  10393  canthp1lem2  10738  ciclcl  17977  txcmplem1  23960  txlm  23967  dvbsss  26222  nvvcop  31196  nvvop  31211  fldextfld1  34279  prsdm  34546  linedegen  36908  bj-opelresdm  38067  bj-idres  38082  opelopab3  38653  et-ltneverrefl  47881  fuco1  50429  fuco2  50431  fucoid2  50457  fucocolem2  50462  reldmlan2  50725  reldmran2  50726  lanrcl  50729  ranrcl  50730