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

Theorem opeq1 3898
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 2426 . . . 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 3740 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3798 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3806 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2367 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3676 . 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 3895 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3895 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2423 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1647    e. wcel 1715   _Vcvv 2873   (/)c0 3543   ifcif 3654   {csn 3729   {cpr 3730   <.cop 3732
This theorem is referenced by:  opeq12  3900  opeq1i  3901  opeq1d  3904  oteq1  3907  breq1  4128  cbvopab1  4191  cbvopab1s  4193  opthg  4349  eqvinop  4354  opelopabsb  4378  opelxp  4822  elvvv  4852  opabid2  4918  opeliunxp2  4927  elsnres  5094  elimasng  5142  dmsnopg  5247  cnvsng  5261  elxp4  5263  elxp5  5264  funopg  5389  f1osng  5620  f1oprswap  5621  dmfco  5700  fvelrn  5768  fsng  5808  fprg  5816  fvsng  5827  funfvima3  5875  opabex3d  5889  opabex3  5890  oveq1  5988  oprabid  6005  dfoprab2  6021  cbvoprab1  6044  op1stg  6259  op2ndg  6260  dfoprab4f  6305  frxp  6353  tfrlem11  6546  omeu  6725  oeeui  6742  elixpsn  6998  fundmen  7077  xpsnen  7089  xpassen  7099  xpf1o  7166  unxpdomlem1  7210  dfac5lem1  7897  dfac5lem4  7900  axdc4lem  8228  nqereu  8700  mulcanenq  8731  archnq  8751  prlem934  8804  supsrlem  8880  supsr  8881  fsum2dlem  12441  vdwlem10  13245  imasaddfnlem  13640  catideu  13787  iscatd2  13793  catlid  13795  catpropd  13822  efgmval  15231  efgi  15238  vrgpval  15286  gsumcom2  15436  txkgen  17563  cnmpt21  17582  xkoinjcn  17598  txcon  17600  pt1hmeo  17714  divstgplem  18016  dvbsss  19467  drngoi  21385  isdivrngo  21409  isnvlem  21479  cnextfvval  23701  br8  24854  br6  24855  br4  24856  eldm3  24860  dfdm5  24873  brimg  25217  brapply  25218  brrestrict  25229  dfrdg4  25230  axlowdim2  25330  axlowdim  25331  axcontlem10  25343  axcontlem12  25345  cgrdegen  25369  brofs  25370  cgrextend  25373  brifs  25408  ifscgr  25409  brcgr3  25411  brcolinear2  25423  colineardim1  25426  brfs  25444  idinside  25449  btwnconn1lem7  25458  btwnconn1lem11  25462  btwnconn1lem12  25463  brsegle  25473  outsideofeu  25496  fvray  25506  linedegen  25508  fvline  25509  dropab1  27156  relopabVD  28441  dicelval3  31441  dihjatcclem4  31682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 937  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-rab 2637  df-v 2875  df-dif 3241  df-un 3243  df-in 3245  df-ss 3252  df-nul 3544  df-if 3655  df-sn 3735  df-pr 3736  df-op 3738
  Copyright terms: Public domain W3C validator