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

Theorem opeq1 3926
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 2447 . . . 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 3768 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3826 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3834 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2388 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3704 . 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 3923 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3923 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2444 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717   _Vcvv 2899   (/)c0 3571   ifcif 3682   {csn 3757   {cpr 3758   <.cop 3760
This theorem is referenced by:  opeq12  3928  opeq1i  3929  opeq1d  3932  oteq1  3935  breq1  4156  cbvopab1  4219  cbvopab1s  4221  opthg  4377  eqvinop  4382  opelopabsb  4406  opelxp  4848  elvvv  4877  opabid2  4944  opeliunxp2  4953  elsnres  5122  elimasng  5170  dmsnopg  5281  cnvsng  5295  elxp4  5297  elxp5  5298  funopg  5425  f1osng  5656  f1oprswap  5657  dmfco  5736  fvelrn  5805  fsng  5846  fprg  5854  fvsng  5866  funfvima3  5914  opabex3d  5928  opabex3  5929  oveq1  6027  oprabid  6044  dfoprab2  6060  cbvoprab1  6083  op1stg  6298  op2ndg  6299  dfoprab4f  6344  frxp  6392  tfrlem11  6585  omeu  6764  oeeui  6781  elixpsn  7037  fundmen  7116  xpsnen  7128  xpassen  7138  xpf1o  7205  unxpdomlem1  7249  dfac5lem1  7937  dfac5lem4  7940  axdc4lem  8268  nqereu  8739  mulcanenq  8770  archnq  8790  prlem934  8843  supsrlem  8919  supsr  8920  fsum2dlem  12481  vdwlem10  13285  imasaddfnlem  13680  catideu  13827  iscatd2  13833  catlid  13835  catpropd  13862  efgmval  15271  efgi  15278  vrgpval  15326  gsumcom2  15476  txkgen  17605  cnmpt21  17624  xkoinjcn  17640  txcon  17642  pt1hmeo  17759  cnextfvval  18017  divstgplem  18071  dvbsss  19656  drngoi  21843  isdivrngo  21867  isnvlem  21937  br8  25137  br6  25138  br4  25139  eldm3  25143  dfdm5  25156  brimg  25500  brapply  25501  brrestrict  25512  dfrdg4  25513  axlowdim2  25613  axlowdim  25614  axcontlem10  25626  axcontlem12  25628  cgrdegen  25652  brofs  25653  cgrextend  25656  brifs  25691  ifscgr  25692  brcgr3  25694  brcolinear2  25706  colineardim1  25709  brfs  25727  idinside  25732  btwnconn1lem7  25741  btwnconn1lem11  25745  btwnconn1lem12  25746  brsegle  25756  outsideofeu  25779  fvray  25789  linedegen  25791  fvline  25792  dropab1  27318  relopabVD  28354  dicelval3  31295  dihjatcclem4  31536
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766
  Copyright terms: Public domain W3C validator