Theorem opelxp1 4886

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	|- ( <. A , B >. e. ( C X. D ) -> A e. C )

Proof of Theorem opelxp1

Step	Hyp	Ref	Expression
1		opelxp 4883	. 2 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
2	1	simplbi 466	1 |- ( <. A , B >. e. ( C X. D ) -> A e. C )

Syntax hints:   -> wi 4   e. wcel 1898   <.cop 3986   X. cxp 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4476  df-xp 4859

This theorem is referenced by:  otelxp1  4888  dff3  6058  ressnop0  6095  swoord1  7418  swoord2  7419  canthp1lem2  9104  ciclcl  15756  txcmplem1  20705  txlm  20712  dvbsss  22906  vcoprnelem  26246  nvvcop  26262  nvvop  26277  prsdm  28769  linedegen  30959  opelopab3  32088