Theorem opelxp1 4891

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 4888	. 2 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
2	1	simplbi 460	1 |- ( <. A , B >. e. ( C X. D ) -> A e. C )

Syntax hints:   -> wi 4   e. wcel 1756   <.cop 3902   X. cxp 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pr 4550

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-rab 2743  df-v 2993  df-dif 3350  df-un 3352  df-in 3354  df-ss 3361  df-nul 3657  df-if 3811  df-sn 3897  df-pr 3899  df-op 3903  df-opab 4370  df-xp 4865

This theorem is referenced by:  otelxp1  4893  dff3  5875  ressnop0  5908  swoord1  7149  swoord2  7150  canthp1lem2  8839  txcmplem1  19233  txlm  19240  dvbsss  21396  vcoprnelem  23975  nvvcop  23991  nvvop  24006  prsdm  26363  linedegen  28193  opelopab3  28633