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

Theorem opeq2 3987
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 2498 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 686 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 3886 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 3892 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
5 eqidd 2439 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
62, 4, 5ifbieq12d 3763 . 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 3983 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
8 dfopif 3983 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
96, 7, 83eqtr4g 2495 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   _Vcvv 2958   (/)c0 3630   ifcif 3741   {csn 3816   {cpr 3817   <.cop 3819
This theorem is referenced by:  opeq12  3988  opeq2i  3990  opeq2d  3993  oteq2  3996  oteq3  3997  breq2  4218  cbvopab2  4281  cbvopab2v  4284  opthg  4438  eqvinop  4443  opelopabsb  4467  dfid3  4501  opelxp  4910  opabid2  5006  elrn2g  5063  opeldm  5075  elrn2  5111  opelresg  5155  iss  5191  elimasng  5232  issref  5249  dmsnopg  5343  cnvsng  5357  elxp4  5359  elxp5  5360  funopg  5487  f1osng  5718  f1oprswap  5719  tz6.12f  5751  fsn  5908  fsng  5909  fprg  5917  fvsng  5929  opabex3d  5991  opabex3  5992  oveq2  6091  cbvoprab2  6147  ovg  6214  op1stg  6361  op2ndg  6362  op1steq  6393  dfoprab4f  6407  seqomlem2  6710  omeu  6830  oeeui  6847  elixpsn  7103  ixpsnf1o  7104  mapsnen  7186  xpsnen  7194  xpassen  7204  xpf1o  7271  unxpdomlem1  7315  axdc4lem  8337  nqereu  8808  mulcanenq  8839  elreal  9008  ax1rid  9038  fseq1p1m1  11124  ruclem1  12832  imasaddfnlem  13755  imasvscafn  13764  catidex  13901  catpropd  13937  efgi  15353  gsumcom2  15551  txkgen  17686  cnmpt21  17705  xkoinjcn  17721  txcon  17723  xpstopnlem1  17843  divstgplem  18152  metustidOLD  18591  metustid  18592  1pthoncl  21594  2pthoncl  21605  drngoi  21997  isdivrngo  22021  vcoprne  22060  isnvlem  22091  cvmlift2lem1  24991  cvmlift2lem12  25003  br8  25381  br6  25382  br4  25383  fprb  25399  dfrn5  25403  elima4  25406  pprodss4v  25731  brimg  25784  brapply  25785  brrestrict  25796  dfrdg4  25797  axlowdim2  25901  axlowdim  25902  axcontlem2  25906  axcontlem3  25907  axcontlem4  25908  axcontlem9  25913  axcontlem10  25914  axcontlem11  25915  cgrtriv  25938  brofs  25941  segconeu  25947  btwntriv2  25948  transportprops  25970  brifs  25979  ifscgr  25980  brcgr3  25982  cgrxfr  25991  brcolinear2  25994  colineardim1  25997  brfs  26015  idinside  26020  btwnconn1lem7  26029  btwnconn1lem11  26033  btwnconn1lem12  26034  btwnconn1lem14  26036  brsegle  26044  seglerflx  26048  seglemin  26049  segleantisym  26051  btwnsegle  26053  outsideofeu  26067  outsidele  26068  linedegen  26079  fvline  26080  ralxpmap  26744  psgnunilem5  27396  dropab2  27629  swrdccatin1  28227  swrdccat3blem  28240  swrdccatin12d  28244  cshfn  28256  0eusgraiff0rgra  28438  relopabVD  29075  bnj941  29205  bnj944  29371  dibelval3  32007  diblsmopel  32031  dihjatcclem4  32281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825
  Copyright terms: Public domain W3C validator