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

Theorem opeq2 4214
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 2539 . . . 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 4107 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 4113 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3962 . 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 4210 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4210 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2533 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   _Vcvv 3113   (/)c0 3785   ifcif 3939   {csn 4027   {cpr 4029   <.cop 4033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034
This theorem is referenced by:  opeq12  4215  opeq2i  4217  opeq2d  4220  oteq2  4223  oteq3  4224  breq2  4451  cbvopab2  4518  cbvopab2v  4521  opthg  4722  eqvinop  4731  opelopabsb  4757  dfid3  4796  opelxp  5029  opabid2  5132  elrn2g  5193  opeldm  5206  elrn2  5242  opelresg  5281  iss  5321  elimasng  5363  issref  5380  dmsnopg  5479  cnvsng  5494  funopg  5620  f1osng  5854  f1oprswap  5855  tz6.12f  5884  fsn  6059  fsng  6060  fprg  6070  fvsng  6095  oveq2  6292  cbvoprab2  6354  ovg  6425  elxp4  6728  elxp5  6729  opabex3d  6762  opabex3  6763  op1stg  6796  op2ndg  6797  op1steq  6826  dfoprab4f  6842  seqomlem2  7116  omeu  7234  oeeui  7251  ralxpmap  7468  elixpsn  7508  ixpsnf1o  7509  mapsnen  7593  xpsnen  7601  xpassen  7611  xpf1o  7679  unxpdomlem1  7724  axdc4lem  8835  nqereu  9307  mulcanenq  9338  elreal  9508  ax1rid  9538  fseq1p1m1  11752  swrdccatin1  12671  swrdccat3blem  12683  swrdccatid  12685  swrdccatin12d  12689  wrdlen2  12849  ruclem1  13825  imasaddfnlem  14783  imasvscafn  14792  catidex  14929  catpropd  14965  symg2bas  16228  psgnunilem5  16325  efgi  16543  gsumcom2  16806  mat1rhmval  18776  mat1ric  18784  txkgen  19916  cnmpt21  19935  xkoinjcn  19951  txcon  19953  xpstopnlem1  20073  divstgplem  20382  metustidOLD  20825  metustid  20826  axlowdim2  23967  axlowdim  23968  axcontlem2  23972  axcontlem3  23973  axcontlem4  23974  axcontlem9  23979  axcontlem10  23980  axcontlem11  23981  1pthoncl  24298  2pthoncl  24309  wwlknextbi  24429  wwlkextinj  24434  wwlkextsur  24435  clwwlkfo  24501  0eusgraiff0rgra  24643  drngoi  25113  isdivrngo  25137  vcoprne  25176  isnvlem  25207  br8d  27164  prsdm  27560  eulerpartlemgvv  27983  cvmlift2lem1  28415  cvmlift2lem12  28427  br8  28790  br6  28791  br4  28792  fprb  28808  dfrn5  28812  elima4  28814  pprodss4v  29139  brimg  29192  brapply  29193  brrestrict  29204  dfrdg4  29205  cgrtriv  29257  brofs  29260  segconeu  29266  btwntriv2  29267  transportprops  29289  brifs  29298  ifscgr  29299  brcgr3  29301  cgrxfr  29310  brcolinear2  29313  colineardim1  29316  brfs  29334  idinside  29339  btwnconn1lem7  29348  btwnconn1lem11  29352  btwnconn1lem12  29353  btwnconn1lem14  29355  brsegle  29363  seglerflx  29367  seglemin  29368  segleantisym  29370  btwnsegle  29372  outsideofeu  29386  outsidele  29387  linedegen  29398  fvline  29399  dropab2  30963  relopabVD  32799  bnj941  32928  bnj944  33093  dibelval3  35962  diblsmopel  35986  dihjatcclem4  36236
  Copyright terms: Public domain W3C validator