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

Theorem opeq2 4048
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )

Proof of Theorem opeq2
StepHypRef Expression
1 eleq1 2493 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 696 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 3943 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 3949 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3800 . 2  |-  ( A  =  B  ->  if ( ( C  e. 
_V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) ) )
6 dfopif 4044 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4044 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2490 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1362    e. wcel 1755   _Vcvv 2962   (/)c0 3625   ifcif 3779   {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-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
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-rab 2714  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:  opeq12  4049  opeq2i  4051  opeq2d  4054  oteq2  4057  oteq3  4058  breq2  4284  cbvopab2  4351  cbvopab2v  4354  opthg  4555  eqvinop  4563  opelopabsb  4588  dfid3  4624  opelxp  4856  opabid2  4956  elrn2g  5017  opeldm  5030  elrn2  5066  opelresg  5105  iss  5142  elimasng  5183  issref  5199  dmsnopg  5298  cnvsng  5313  funopg  5438  f1osng  5667  f1oprswap  5668  tz6.12f  5696  fsn  5868  fsng  5869  fprg  5878  fvsng  5899  oveq2  6088  cbvoprab2  6148  ovg  6218  elxp4  6511  elxp5  6512  opabex3d  6544  opabex3  6545  op1stg  6578  op2ndg  6579  op1steq  6607  dfoprab4f  6621  seqomlem2  6892  omeu  7012  oeeui  7029  ralxpmap  7250  elixpsn  7290  ixpsnf1o  7291  mapsnen  7375  xpsnen  7383  xpassen  7393  xpf1o  7461  unxpdomlem1  7505  axdc4lem  8612  nqereu  9085  mulcanenq  9116  elreal  9285  ax1rid  9315  fseq1p1m1  11517  swrdccatin1  12357  swrdccat3blem  12369  swrdccatid  12371  swrdccatin12d  12375  wrdlen2  12531  ruclem1  13495  imasaddfnlem  14448  imasvscafn  14457  catidex  14594  catpropd  14630  symg2bas  15882  psgnunilem5  15979  efgi  16195  gsumcom2  16440  txkgen  19066  cnmpt21  19085  xkoinjcn  19101  txcon  19103  xpstopnlem1  19223  divstgplem  19532  metustidOLD  19975  metustid  19976  axlowdim2  23028  axlowdim  23029  axcontlem2  23033  axcontlem3  23034  axcontlem4  23035  axcontlem9  23040  axcontlem10  23041  axcontlem11  23042  1pthoncl  23313  2pthoncl  23324  drngoi  23716  isdivrngo  23740  vcoprne  23779  isnvlem  23810  br8d  25765  prsdm  26197  eulerpartlemgvv  26606  cvmlift2lem1  27038  cvmlift2lem12  27050  br8  27412  br6  27413  br4  27414  fprb  27430  dfrn5  27434  elima4  27436  pprodss4v  27761  brimg  27814  brapply  27815  brrestrict  27826  dfrdg4  27827  cgrtriv  27879  brofs  27882  segconeu  27888  btwntriv2  27889  transportprops  27911  brifs  27920  ifscgr  27921  brcgr3  27923  cgrxfr  27932  brcolinear2  27935  colineardim1  27938  brfs  27956  idinside  27961  btwnconn1lem7  27970  btwnconn1lem11  27974  btwnconn1lem12  27975  btwnconn1lem14  27977  brsegle  27985  seglerflx  27989  seglemin  27990  segleantisym  27992  btwnsegle  27994  outsideofeu  28008  outsidele  28009  linedegen  28020  fvline  28021  dropab2  29546  wwlknextbi  30200  wwlkextinj  30205  wwlkextsur  30206  clwwlkfo  30302  0eusgraiff0rgra  30395  relopabVD  31336  bnj941  31465  bnj944  31630  dibelval3  34362  diblsmopel  34386  dihjatcclem4  34636
  Copyright terms: Public domain W3C validator