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

Theorem opeq2 4081
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 2503 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 703 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 3976 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 3982 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3833 . 2  |-  ( A  =  B  ->  if ( ( C  e. 
_V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) ) )
6 dfopif 4077 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4077 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2500 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   _Vcvv 2993   (/)c0 3658   ifcif 3812   {csn 3898   {cpr 3900   <.cop 3904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905
This theorem is referenced by:  opeq12  4082  opeq2i  4084  opeq2d  4087  oteq2  4090  oteq3  4091  breq2  4317  cbvopab2  4384  cbvopab2v  4387  opthg  4588  eqvinop  4596  opelopabsb  4620  dfid3  4658  opelxp  4890  opabid2  4990  elrn2g  5051  opeldm  5064  elrn2  5100  opelresg  5139  iss  5175  elimasng  5216  issref  5232  dmsnopg  5331  cnvsng  5346  funopg  5471  f1osng  5700  f1oprswap  5701  tz6.12f  5729  fsn  5902  fsng  5903  fprg  5912  fvsng  5933  oveq2  6120  cbvoprab2  6180  ovg  6250  elxp4  6543  elxp5  6544  opabex3d  6576  opabex3  6577  op1stg  6610  op2ndg  6611  op1steq  6639  dfoprab4f  6653  seqomlem2  6927  omeu  7045  oeeui  7062  ralxpmap  7283  elixpsn  7323  ixpsnf1o  7324  mapsnen  7408  xpsnen  7416  xpassen  7426  xpf1o  7494  unxpdomlem1  7538  axdc4lem  8645  nqereu  9119  mulcanenq  9150  elreal  9319  ax1rid  9349  fseq1p1m1  11555  swrdccatin1  12395  swrdccat3blem  12407  swrdccatid  12409  swrdccatin12d  12413  wrdlen2  12569  ruclem1  13534  imasaddfnlem  14487  imasvscafn  14496  catidex  14633  catpropd  14669  symg2bas  15924  psgnunilem5  16021  efgi  16237  gsumcom2  16489  txkgen  19247  cnmpt21  19266  xkoinjcn  19282  txcon  19284  xpstopnlem1  19404  divstgplem  19713  metustidOLD  20156  metustid  20157  axlowdim2  23228  axlowdim  23229  axcontlem2  23233  axcontlem3  23234  axcontlem4  23235  axcontlem9  23240  axcontlem10  23241  axcontlem11  23242  1pthoncl  23513  2pthoncl  23524  drngoi  23916  isdivrngo  23940  vcoprne  23979  isnvlem  24010  br8d  25964  prsdm  26366  eulerpartlemgvv  26781  cvmlift2lem1  27213  cvmlift2lem12  27225  br8  27588  br6  27589  br4  27590  fprb  27606  dfrn5  27610  elima4  27612  pprodss4v  27937  brimg  27990  brapply  27991  brrestrict  28002  dfrdg4  28003  cgrtriv  28055  brofs  28058  segconeu  28064  btwntriv2  28065  transportprops  28087  brifs  28096  ifscgr  28097  brcgr3  28099  cgrxfr  28108  brcolinear2  28111  colineardim1  28114  brfs  28132  idinside  28137  btwnconn1lem7  28146  btwnconn1lem11  28150  btwnconn1lem12  28151  btwnconn1lem14  28153  brsegle  28161  seglerflx  28165  seglemin  28166  segleantisym  28168  btwnsegle  28170  outsideofeu  28184  outsidele  28185  linedegen  28196  fvline  28197  dropab2  29730  wwlknextbi  30383  wwlkextinj  30388  wwlkextsur  30389  clwwlkfo  30485  0eusgraiff0rgra  30578  relopabVD  31733  bnj941  31862  bnj944  32027  dibelval3  34888  diblsmopel  34912  dihjatcclem4  35162
  Copyright terms: Public domain W3C validator