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  24113  br6  24114  br4  24115  eldm3  24119  dfdm5  24132  brimg  24476  brapply  24477  brrestrict  24487  dfrdg4  24488  axlowdim2  24588  axlowdim  24589  axcontlem10  24601  axcontlem12  24603  cgrdegen  24627  brofs  24628  cgrextend  24631  brifs  24666  ifscgr  24667  brcgr3  24669  brcolinear2  24681  colineardim1  24684  brfs  24702  idinside  24707  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1lem12  24721  brsegle  24731  outsideofeu  24754  fvray  24764  linedegen  24766  fvline  24767  eqvinopb  24965  prj1b  25079  prj3  25080  fprg  25133  isded  25736  dedi  25737  cmppfd  25745  dmrngcmp  25751  iscatOLD  25754  cati  25755  imonclem  25813  dropab1  27650  relopabVD  28677  dicelval3  31370  dihjatcclem4  31611
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