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

Theorem opeq2 3797
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )

Proof of Theorem opeq2
StepHypRef Expression
1 eleq1 2343 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 684 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 3707 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 3713 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
5 eqidd 2284 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
62, 4, 5ifbieq12d 3587 . 2  |-  ( A  =  B  ->  if ( ( C  e. 
_V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) ) )
7 dfopif 3793 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
8 dfopif 3793 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
96, 7, 83eqtr4g 2340 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
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  opeq2i  3800  opeq2d  3803  oteq2  3806  oteq3  3807  breq2  4027  cbvopab2  4090  cbvopab2v  4093  opthg  4246  eqvinop  4251  opelopabsb  4275  dfid3  4310  opelxp  4719  opabid2  4815  elrn2g  4870  opeldm  4882  elrn2  4918  opelresg  4962  iss  4998  elimasng  5039  issref  5056  dmsnopg  5144  cnvsng  5158  elxp4  5160  elxp5  5161  funopg  5286  f1osng  5514  f1oprswap  5515  tz6.12f  5546  fsn  5696  fsng  5697  fvsng  5714  opabex3  5769  oveq2  5866  cbvoprab2  5919  ovg  5986  op1stg  6132  op2ndg  6133  op1steq  6164  dfoprab4f  6178  seqomlem2  6463  omeu  6583  oeeui  6600  elixpsn  6855  ixpsnf1o  6856  mapsnen  6938  xpsnen  6946  xpassen  6956  xpf1o  7023  unxpdomlem1  7067  axdc4lem  8081  nqereu  8553  mulcanenq  8584  elreal  8753  ax1rid  8783  fseq1p1m1  10857  ruclem1  12509  imasaddfnlem  13430  imasvscafn  13439  catidex  13576  catpropd  13612  efgi  15028  gsumcom2  15226  txkgen  17346  cnmpt21  17365  xkoinjcn  17381  txcon  17383  xpstopnlem1  17500  divstgplem  17803  drngoi  21074  isdivrngo  21098  vcoprne  21135  isnvlem  21166  cvmlift2lem1  23833  cvmlift2lem12  23845  br8  24113  br6  24114  br4  24115  fprb  24129  dfrn5  24133  pprodss4v  24424  brimg  24476  brapply  24477  brrestrict  24487  dfrdg4  24488  axlowdim2  24588  axlowdim  24589  axcontlem2  24593  axcontlem3  24594  axcontlem4  24595  axcontlem9  24600  axcontlem10  24601  axcontlem11  24602  cgrtriv  24625  brofs  24628  segconeu  24634  btwntriv2  24635  transportprops  24657  brifs  24666  ifscgr  24667  brcgr3  24669  cgrxfr  24678  brcolinear2  24681  colineardim1  24684  brfs  24702  idinside  24707  btwnconn1lem7  24716  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem14  24723  brsegle  24731  seglerflx  24735  seglemin  24736  segleantisym  24738  btwnsegle  24740  outsideofeu  24754  outsidele  24755  linedegen  24766  fvline  24767  eqvinopb  24965  prj1b  25079  prj3  25080  fprg  25133  repcpwti  25161  cbcpcp  25162  cbicp  25166  isded  25736  dedi  25737  cmppfd  25745  dmrngcmp  25751  iscatOLD  25754  cati  25755  iepiclem  25823  cndpv  26049  pgapspf  26052  pgapspf2  26053  ralxpmap  26761  psgnunilem5  27417  dropab2  27651  relopabVD  28677  bnj941  28804  bnj944  28970  dibelval3  31337  diblsmopel  31361  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