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

Theorem opeq1 3812
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 2356 . . . 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 3664 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3719 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3727 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2297 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3600 . 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 3809 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3809 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2353 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468   ifcif 3578   {csn 3653   {cpr 3654   <.cop 3656
This theorem is referenced by:  opeq12  3814  opeq1i  3815  opeq1d  3818  oteq1  3821  breq1  4042  cbvopab1  4105  cbvopab1s  4107  opthg  4262  eqvinop  4267  opelopabsb  4291  opelxp  4735  elvvv  4765  opabid2  4831  opeliunxp2  4840  elsnres  5007  elimasng  5055  dmsnopg  5160  cnvsng  5174  elxp4  5176  elxp5  5177  funopg  5302  f1osng  5530  f1oprswap  5531  dmfco  5609  fvelrn  5677  fsng  5713  fvsng  5730  funfvima3  5771  opabex3  5785  oveq1  5881  oprabid  5898  dfoprab2  5911  cbvoprab1  5934  op1stg  6148  op2ndg  6149  dfoprab4f  6194  frxp  6241  tfrlem11  6420  omeu  6599  oeeui  6616  elixpsn  6871  fundmen  6950  xpsnen  6962  xpassen  6972  xpf1o  7039  unxpdomlem1  7083  dfac5lem1  7766  dfac5lem4  7769  axdc4lem  8097  nqereu  8569  mulcanenq  8600  archnq  8620  prlem934  8673  supsrlem  8749  supsr  8750  fsum2dlem  12249  vdwlem10  13053  imasaddfnlem  13446  catideu  13593  iscatd2  13599  catlid  13601  catpropd  13628  efgmval  15037  efgi  15044  vrgpval  15092  gsumcom2  15242  txkgen  17362  cnmpt21  17381  xkoinjcn  17397  txcon  17399  pt1hmeo  17513  divstgplem  17819  dvbsss  19268  drngoi  21090  isdivrngo  21114  isnvlem  21182  br8  24184  br6  24185  br4  24186  eldm3  24190  dfdm5  24203  brimg  24547  brapply  24548  brrestrict  24559  dfrdg4  24560  axlowdim2  24660  axlowdim  24661  axcontlem10  24673  axcontlem12  24675  cgrdegen  24699  brofs  24700  cgrextend  24703  brifs  24738  ifscgr  24739  brcgr3  24741  brcolinear2  24753  colineardim1  24756  brfs  24774  idinside  24779  btwnconn1lem7  24788  btwnconn1lem11  24792  btwnconn1lem12  24793  brsegle  24803  outsideofeu  24826  fvray  24836  linedegen  24838  fvline  24839  eqvinopb  25068  prj1b  25182  prj3  25183  fprg  25236  isded  25839  dedi  25840  cmppfd  25848  dmrngcmp  25854  iscatOLD  25857  cati  25858  imonclem  25916  dropab1  27753  opabex3d  28190  relopabVD  28993  dicelval3  31992  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662
  Copyright terms: Public domain W3C validator