MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opth1 Structured version   Unicode version

Theorem opth1 4553
Description: Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
Hypotheses
Ref Expression
opth1.1  |-  A  e. 
_V
opth1.2  |-  B  e. 
_V
Assertion
Ref Expression
opth1  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )

Proof of Theorem opth1
StepHypRef Expression
1 opth1.1 . . . 4  |-  A  e. 
_V
21sneqr 4028 . . 3  |-  ( { A }  =  { C }  ->  A  =  C )
32a1i 11 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( { A }  =  { C }  ->  A  =  C ) )
4 opth1.2 . . . . . . . . 9  |-  B  e. 
_V
51, 4opi1 4547 . . . . . . . 8  |-  { A }  e.  <. A ,  B >.
6 id 22 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  D >. )
75, 6syl5eleq 2519 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  <. C ,  D >. )
8 oprcl 4072 . . . . . . 7  |-  ( { A }  e.  <. C ,  D >.  ->  ( C  e.  _V  /\  D  e.  _V ) )
97, 8syl 16 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( C  e.  _V  /\  D  e.  _V )
)
109simpld 456 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  _V )
11 prid1g 3969 . . . . 5  |-  ( C  e.  _V  ->  C  e.  { C ,  D } )
1210, 11syl 16 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  { C ,  D } )
13 eleq2 2494 . . . 4  |-  ( { A }  =  { C ,  D }  ->  ( C  e.  { A }  <->  C  e.  { C ,  D } ) )
1412, 13syl5ibrcom 222 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( { A }  =  { C ,  D }  ->  C  e.  { A } ) )
15 elsni 3890 . . . 4  |-  ( C  e.  { A }  ->  C  =  A )
1615eqcomd 2438 . . 3  |-  ( C  e.  { A }  ->  A  =  C )
1714, 16syl6 33 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( { A }  =  { C ,  D }  ->  A  =  C ) )
18 dfopg 4045 . . . . 5  |-  ( ( C  e.  _V  /\  D  e.  _V )  -> 
<. C ,  D >.  =  { { C } ,  { C ,  D } } )
197, 8, 183syl 20 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  D } } )
207, 19eleqtrd 2509 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  { { C } ,  { C ,  D } } )
21 elpri 3885 . . 3  |-  ( { A }  e.  { { C } ,  { C ,  D } }  ->  ( { A }  =  { C }  \/  { A }  =  { C ,  D } ) )
2220, 21syl 16 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( { A }  =  { C }  \/  { A }  =  { C ,  D }
) )
233, 17, 22mpjaod 381 1  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    /\ wa 369    = wceq 1362    e. wcel 1755   _Vcvv 2962   {csn 3865   {cpr 3867   <.cop 3871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872
This theorem is referenced by:  opth  4554  dmsnopg  5298  funcnvsn  5451  oprabid  6104  seqomlem2  6892  unxpdomlem3  7507  dfac5lem4  8284  dcomex  8604  canthwelem  8805  uzrdgfni  11765  gsum2d2  16440  2trllemA  23272  2pthon  23324  2pthon3v  23326  constr3lem2  23355
  Copyright terms: Public domain W3C validator