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

Theorem opeq1 3756
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 2316 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 688 . . 3  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3611 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3666 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3674 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2257 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3547 . 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 3753 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3753 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2313 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2757   (/)c0 3416   ifcif 3525   {csn 3600   {cpr 3601   <.cop 3603
This theorem is referenced by:  opeq12  3758  opeq1i  3759  opeq1d  3762  oteq1  3765  breq1  3986  cbvopab1  4049  cbvopab1s  4051  opthg  4204  eqvinop  4209  opelopabsb  4233  opelxp  4693  elvvv  4723  opabid2  4789  opeliunxp2  4798  elsnres  4965  elimasng  5013  dmsnopg  5117  cnvsng  5131  elxp4  5133  elxp5  5134  funopg  5211  f1osng  5438  f1oprswap  5439  dmfco  5513  fvelrn  5581  fsng  5617  fvsng  5634  funfvima3  5675  opabex3  5689  oveq1  5785  oprabid  5802  dfoprab2  5815  cbvoprab1  5838  op1stg  6052  op2ndg  6053  dfoprab4f  6098  frxp  6145  tfrlem11  6358  omeu  6537  oeeui  6554  elixpsn  6809  fundmen  6888  xpsnen  6900  xpassen  6910  xpf1o  6977  unxpdomlem1  7021  dfac5lem1  7704  dfac5lem4  7707  axdc4lem  8035  nqereu  8507  mulcanenq  8538  archnq  8558  prlem934  8611  supsrlem  8687  supsr  8688  fsum2dlem  12184  vdwlem10  12985  imasaddfnlem  13378  catideu  13525  iscatd2  13531  catlid  13533  catpropd  13560  efgmval  14969  efgi  14976  vrgpval  15024  gsumcom2  15174  txkgen  17294  cnmpt21  17313  xkoinjcn  17329  txcon  17331  pt1hmeo  17445  divstgplem  17751  dvbsss  19200  drngoi  21020  isdivrngo  21044  isnvlem  21112  br8  23470  br6  23471  br4  23472  dfdm5  23487  elfuns  23815  brimg  23837  brapply  23838  brrestrict  23848  dfrdg4  23849  axlowdim2  23949  axlowdim  23950  axcontlem10  23962  axcontlem12  23964  cgrdegen  23988  brofs  23989  cgrextend  23992  brifs  24027  ifscgr  24028  brcgr3  24030  brcolinear2  24042  colineardim1  24045  brfs  24063  idinside  24068  btwnconn1lem7  24077  btwnconn1lem11  24081  btwnconn1lem12  24082  brsegle  24092  outsideofeu  24115  fvray  24125  linedegen  24127  fvline  24128  eqvinopb  24317  prj1b  24431  prj3  24432  fprg  24486  isded  25089  dedi  25090  cmppfd  25098  dmrngcmp  25104  iscatOLD  25107  cati  25108  imonclem  25166  dropab1  27004  relopabVD  27711  dicelval3  30521  dihjatcclem4  30762
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609
  Copyright terms: Public domain W3C validator