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

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

Proof of Theorem opeq1
StepHypRef Expression
1 eleq1 2495 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 686 . . 3  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3817 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3875 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3883 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2436 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3753 . 2  |-  ( A  =  B  ->  if ( ( A  e. 
_V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) ) )
8 dfopif 3973 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3973 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2492 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725   _Vcvv 2948   (/)c0 3620   ifcif 3731   {csn 3806   {cpr 3807   <.cop 3809
This theorem is referenced by:  opeq12  3978  opeq1i  3979  opeq1d  3982  oteq1  3985  breq1  4207  cbvopab1  4270  cbvopab1s  4272  opthg  4428  eqvinop  4433  opelopabsb  4457  opelxp  4899  elvvv  4928  opabid2  4995  opeliunxp2  5004  elsnres  5173  elimasng  5221  dmsnopg  5332  cnvsng  5346  elxp4  5348  elxp5  5349  funopg  5476  f1osng  5707  f1oprswap  5708  dmfco  5788  fvelrn  5857  fsng  5898  fprg  5906  fvsng  5918  funfvima3  5966  opabex3d  5980  opabex3  5981  oveq1  6079  oprabid  6096  dfoprab2  6112  cbvoprab1  6135  op1stg  6350  op2ndg  6351  dfoprab4f  6396  frxp  6447  tfrlem11  6640  omeu  6819  oeeui  6836  elixpsn  7092  fundmen  7171  xpsnen  7183  xpassen  7193  xpf1o  7260  unxpdomlem1  7304  dfac5lem1  7993  dfac5lem4  7996  axdc4lem  8324  nqereu  8795  mulcanenq  8826  archnq  8846  prlem934  8899  supsrlem  8975  supsr  8976  fsum2dlem  12542  vdwlem10  13346  imasaddfnlem  13741  catideu  13888  iscatd2  13894  catlid  13896  catpropd  13923  efgmval  15332  efgi  15339  vrgpval  15387  gsumcom2  15537  txkgen  17672  cnmpt21  17691  xkoinjcn  17707  txcon  17709  pt1hmeo  17826  cnextfvval  18084  divstgplem  18138  dvbsss  19777  drngoi  21983  isdivrngo  22007  isnvlem  22077  fprod2dlem  25293  br8  25368  br6  25369  br4  25370  eldm3  25374  dfdm5  25387  brimg  25732  brapply  25733  brrestrict  25744  dfrdg4  25745  axlowdim2  25847  axlowdim  25848  axcontlem10  25860  axcontlem12  25862  cgrdegen  25886  brofs  25887  cgrextend  25890  brifs  25925  ifscgr  25926  brcgr3  25928  brcolinear2  25940  colineardim1  25943  brfs  25961  idinside  25966  btwnconn1lem7  25975  btwnconn1lem11  25979  btwnconn1lem12  25980  brsegle  25990  outsideofeu  26013  fvray  26023  linedegen  26025  fvline  26026  dropab1  27564  el2xptp  27996  swrdccatin1  28091  shwrd  28120  relopabVD  28867  dicelval3  31817  dihjatcclem4  32058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815
  Copyright terms: Public domain W3C validator