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

Theorem opeq1 3796
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 2343 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 685 . . 3  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3651 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3706 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3714 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2284 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3587 . 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 3793 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3793 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2340 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   _Vcvv 2788   (/)c0 3455   ifcif 3565   {csn 3640   {cpr 3641   <.cop 3643
This theorem is referenced by:  opeq12  3798  opeq1i  3799  opeq1d  3802  oteq1  3805  breq1  4026  cbvopab1  4089  cbvopab1s  4091  opthg  4246  eqvinop  4251  opelopabsb  4275  opelxp  4719  elvvv  4749  opabid2  4815  opeliunxp2  4824  elsnres  4991  elimasng  5039  dmsnopg  5144  cnvsng  5158  elxp4  5160  elxp5  5161  funopg  5286  f1osng  5514  f1oprswap  5515  dmfco  5593  fvelrn  5661  fsng  5697  fvsng  5714  funfvima3  5755  opabex3  5769  oveq1  5865  oprabid  5882  dfoprab2  5895  cbvoprab1  5918  op1stg  6132  op2ndg  6133  dfoprab4f  6178  frxp  6225  tfrlem11  6404  omeu  6583  oeeui  6600  elixpsn  6855  fundmen  6934  xpsnen  6946  xpassen  6956  xpf1o  7023  unxpdomlem1  7067  dfac5lem1  7750  dfac5lem4  7753  axdc4lem  8081  nqereu  8553  mulcanenq  8584  archnq  8604  prlem934  8657  supsrlem  8733  supsr  8734  fsum2dlem  12233  vdwlem10  13037  imasaddfnlem  13430  catideu  13577  iscatd2  13583  catlid  13585  catpropd  13612  efgmval  15021  efgi  15028  vrgpval  15076  gsumcom2  15226  txkgen  17346  cnmpt21  17365  xkoinjcn  17381  txcon  17383  pt1hmeo  17497  divstgplem  17803  dvbsss  19252  drngoi  21074  isdivrngo  21098  isnvlem  21166  br8  23524  br6  23525  br4  23526  eldm3  23530  dfdm5  23543  brimg  23887  brapply  23888  brrestrict  23898  dfrdg4  23899  axlowdim2  23999  axlowdim  24000  axcontlem10  24012  axcontlem12  24014  cgrdegen  24038  brofs  24039  cgrextend  24042  brifs  24077  ifscgr  24078  brcgr3  24080  brcolinear2  24092  colineardim1  24095  brfs  24113  idinside  24118  btwnconn1lem7  24127  btwnconn1lem11  24131  btwnconn1lem12  24132  brsegle  24142  outsideofeu  24165  fvray  24175  linedegen  24177  fvline  24178  eqvinopb  24377  prj1b  24491  prj3  24492  fprg  24545  isded  25148  dedi  25149  cmppfd  25157  dmrngcmp  25163  iscatOLD  25166  cati  25167  imonclem  25225  dropab1  27062  relopabVD  28050  dicelval3  30743  dihjatcclem4  30984
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649
  Copyright terms: Public domain W3C validator