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

Theorem opeq2 3813
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 2356 . . . 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 3720 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 3726 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
5 eqidd 2297 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
62, 4, 5ifbieq12d 3600 . 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 3809 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
8 dfopif 3809 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
96, 7, 83eqtr4g 2353 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468   ifcif 3578   {csn 3653   {cpr 3654   <.cop 3656
This theorem is referenced by:  opeq12  3814  opeq2i  3816  opeq2d  3819  oteq2  3822  oteq3  3823  breq2  4043  cbvopab2  4106  cbvopab2v  4109  opthg  4262  eqvinop  4267  opelopabsb  4291  dfid3  4326  opelxp  4735  opabid2  4831  elrn2g  4886  opeldm  4898  elrn2  4934  opelresg  4978  iss  5014  elimasng  5055  issref  5072  dmsnopg  5160  cnvsng  5174  elxp4  5176  elxp5  5177  funopg  5302  f1osng  5530  f1oprswap  5531  tz6.12f  5562  fsn  5712  fsng  5713  fvsng  5730  opabex3  5785  oveq2  5882  cbvoprab2  5935  ovg  6002  op1stg  6148  op2ndg  6149  op1steq  6180  dfoprab4f  6194  seqomlem2  6479  omeu  6599  oeeui  6616  elixpsn  6871  ixpsnf1o  6872  mapsnen  6954  xpsnen  6962  xpassen  6972  xpf1o  7039  unxpdomlem1  7083  axdc4lem  8097  nqereu  8569  mulcanenq  8600  elreal  8769  ax1rid  8799  fseq1p1m1  10873  ruclem1  12525  imasaddfnlem  13446  imasvscafn  13455  catidex  13592  catpropd  13628  efgi  15044  gsumcom2  15242  txkgen  17362  cnmpt21  17381  xkoinjcn  17397  txcon  17399  xpstopnlem1  17516  divstgplem  17819  drngoi  21090  isdivrngo  21114  vcoprne  21151  isnvlem  21182  cvmlift2lem1  23848  cvmlift2lem12  23860  br8  24184  br6  24185  br4  24186  fprb  24200  dfrn5  24204  pprodss4v  24495  brimg  24547  brapply  24548  brrestrict  24559  dfrdg4  24560  axlowdim2  24660  axlowdim  24661  axcontlem2  24665  axcontlem3  24666  axcontlem4  24667  axcontlem9  24672  axcontlem10  24673  axcontlem11  24674  cgrtriv  24697  brofs  24700  segconeu  24706  btwntriv2  24707  transportprops  24729  brifs  24738  ifscgr  24739  brcgr3  24741  cgrxfr  24750  brcolinear2  24753  colineardim1  24756  brfs  24774  idinside  24779  btwnconn1lem7  24788  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn1lem14  24795  brsegle  24803  seglerflx  24807  seglemin  24808  segleantisym  24810  btwnsegle  24812  outsideofeu  24826  outsidele  24827  linedegen  24838  fvline  24839  eqvinopb  25068  prj1b  25182  prj3  25183  fprg  25236  repcpwti  25264  cbcpcp  25265  cbicp  25269  isded  25839  dedi  25840  cmppfd  25848  dmrngcmp  25854  iscatOLD  25857  cati  25858  iepiclem  25926  cndpv  26152  pgapspf  26155  pgapspf2  26156  ralxpmap  26864  psgnunilem5  27520  dropab2  27754  opabex3d  28190  relopabVD  28993  bnj941  29120  bnj944  29286  dibelval3  31959  diblsmopel  31983  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662
  Copyright terms: Public domain W3C validator