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

Theorem opeq2 3945
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 2464 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 685 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 3844 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 3850 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
5 eqidd 2405 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
62, 4, 5ifbieq12d 3721 . 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 3941 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
8 dfopif 3941 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
96, 7, 83eqtr4g 2461 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   _Vcvv 2916   (/)c0 3588   ifcif 3699   {csn 3774   {cpr 3775   <.cop 3777
This theorem is referenced by:  opeq12  3946  opeq2i  3948  opeq2d  3951  oteq2  3954  oteq3  3955  breq2  4176  cbvopab2  4239  cbvopab2v  4242  opthg  4396  eqvinop  4401  opelopabsb  4425  dfid3  4459  opelxp  4867  opabid2  4963  elrn2g  5020  opeldm  5032  elrn2  5068  opelresg  5112  iss  5148  elimasng  5189  issref  5206  dmsnopg  5300  cnvsng  5314  elxp4  5316  elxp5  5317  funopg  5444  f1osng  5675  f1oprswap  5676  tz6.12f  5708  fsn  5865  fsng  5866  fprg  5874  fvsng  5886  opabex3d  5948  opabex3  5949  oveq2  6048  cbvoprab2  6104  ovg  6171  op1stg  6318  op2ndg  6319  op1steq  6350  dfoprab4f  6364  seqomlem2  6667  omeu  6787  oeeui  6804  elixpsn  7060  ixpsnf1o  7061  mapsnen  7143  xpsnen  7151  xpassen  7161  xpf1o  7228  unxpdomlem1  7272  axdc4lem  8291  nqereu  8762  mulcanenq  8793  elreal  8962  ax1rid  8992  fseq1p1m1  11077  ruclem1  12785  imasaddfnlem  13708  imasvscafn  13717  catidex  13854  catpropd  13890  efgi  15306  gsumcom2  15504  txkgen  17637  cnmpt21  17656  xkoinjcn  17672  txcon  17674  xpstopnlem1  17794  divstgplem  18103  metustidOLD  18542  metustid  18543  1pthoncl  21545  2pthoncl  21556  drngoi  21948  isdivrngo  21972  vcoprne  22011  isnvlem  22042  cvmlift2lem1  24942  cvmlift2lem12  24954  br8  25327  br6  25328  br4  25329  fprb  25343  dfrn5  25347  pprodss4v  25638  brimg  25690  brapply  25691  brrestrict  25702  dfrdg4  25703  axlowdim2  25803  axlowdim  25804  axcontlem2  25808  axcontlem3  25809  axcontlem4  25810  axcontlem9  25815  axcontlem10  25816  axcontlem11  25817  cgrtriv  25840  brofs  25843  segconeu  25849  btwntriv2  25850  transportprops  25872  brifs  25881  ifscgr  25882  brcgr3  25884  cgrxfr  25893  brcolinear2  25896  colineardim1  25899  brfs  25917  idinside  25922  btwnconn1lem7  25931  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn1lem14  25938  brsegle  25946  seglerflx  25950  seglemin  25951  segleantisym  25953  btwnsegle  25955  outsideofeu  25969  outsidele  25970  linedegen  25981  fvline  25982  ralxpmap  26632  psgnunilem5  27285  dropab2  27518  swrdccatin1  28016  swrdccatin12b  28027  swrdccatin12c  28028  relopabVD  28722  bnj941  28849  bnj944  29015  dibelval3  31630  diblsmopel  31654  dihjatcclem4  31904
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783
  Copyright terms: Public domain W3C validator