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

Theorem opeq2 4203
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 2515 . . . 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 4095 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 4101 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3949 . 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 4199 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4199 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2509 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804   _Vcvv 3095   (/)c0 3770   ifcif 3926   {csn 4014   {cpr 4016   <.cop 4020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021
This theorem is referenced by:  opeq12  4204  opeq2i  4206  opeq2d  4209  oteq2  4212  oteq3  4213  breq2  4441  cbvopab2  4508  cbvopab2v  4511  opthg  4712  eqvinop  4721  opelopabsb  4747  dfid3  4786  opelxp  5019  opabid2  5122  elrn2g  5183  opeldm  5196  elrn2  5232  opelresg  5271  iss  5311  elimasng  5353  issref  5370  dmsnopg  5469  cnvsng  5484  funopg  5610  f1osng  5844  f1oprswap  5845  tz6.12f  5874  fvn0ssdmfun  6007  fsn  6054  fsng  6055  fprg  6065  fvsng  6090  oveq2  6289  cbvoprab2  6355  ovg  6426  elxp4  6729  elxp5  6730  opabex3d  6763  opabex3  6764  op1stg  6797  op2ndg  6798  op1steq  6827  dfoprab4f  6843  seqomlem2  7118  omeu  7236  oeeui  7253  ralxpmap  7470  elixpsn  7510  ixpsnf1o  7511  mapsnen  7595  xpsnen  7603  xpassen  7613  xpf1o  7681  unxpdomlem1  7726  axdc4lem  8838  nqereu  9310  mulcanenq  9341  elreal  9511  ax1rid  9541  fseq1p1m1  11762  swrdccatin1  12689  swrdccat3blem  12701  swrdccatid  12703  swrdccatin12d  12707  wrdlen2  12867  ruclem1  13945  imasaddfnlem  14906  imasvscafn  14915  catidex  15052  catpropd  15085  symg2bas  16401  psgnunilem5  16497  efgi  16715  gsumcom2  16981  mat1rhmval  18958  mat1ric  18966  txkgen  20130  cnmpt21  20149  xkoinjcn  20165  txcon  20167  xpstopnlem1  20287  qustgplem  20596  metustidOLD  21039  metustid  21040  axlowdim2  24239  axlowdim  24240  axcontlem2  24244  axcontlem3  24245  axcontlem4  24246  axcontlem9  24251  axcontlem10  24252  axcontlem11  24253  1pthoncl  24570  2pthoncl  24581  wwlknextbi  24701  wwlkextinj  24706  wwlkextsur  24707  clwwlkfo  24773  0eusgraiff0rgra  24915  drngoi  25385  isdivrngo  25409  vcoprne  25448  isnvlem  25479  br8d  27439  prsdm  27873  eulerpartlemgvv  28292  cvmlift2lem1  28724  cvmlift2lem12  28736  br8  29160  br6  29161  br4  29162  fprb  29178  dfrn5  29182  elima4  29184  pprodss4v  29509  brimg  29562  brapply  29563  brrestrict  29574  dfrdg4  29575  cgrtriv  29627  brofs  29630  segconeu  29636  btwntriv2  29637  transportprops  29659  brifs  29668  ifscgr  29669  brcgr3  29671  cgrxfr  29680  brcolinear2  29683  colineardim1  29686  brfs  29704  idinside  29709  btwnconn1lem7  29718  btwnconn1lem11  29722  btwnconn1lem12  29723  btwnconn1lem14  29725  brsegle  29733  seglerflx  29737  seglemin  29738  segleantisym  29740  btwnsegle  29742  outsideofeu  29756  outsidele  29757  linedegen  29768  fvline  29769  dropab2  31311  relopabVD  33434  bnj941  33564  bnj944  33729  dibelval3  36614  diblsmopel  36638  dihjatcclem4  36888  dfhe3  37486
  Copyright terms: Public domain W3C validator