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

Theorem opeq2 4180
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 2527 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 715 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 preq2 4064 . . . 4  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
43preq2d 4070 . . 3  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
52, 4ifbieq1d 3915 . 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 4176 . 2  |-  <. C ,  A >.  =  if ( ( C  e.  _V  /\  A  e.  _V ) ,  { { C } ,  { C ,  A } } ,  (/) )
7 dfopif 4176 . 2  |-  <. C ,  B >.  =  if ( ( C  e.  _V  /\  B  e.  _V ) ,  { { C } ,  { C ,  B } } ,  (/) )
85, 6, 73eqtr4g 2520 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1454    e. wcel 1897   _Vcvv 3056   (/)c0 3742   ifcif 3892   {csn 3979   {cpr 3981   <.cop 3985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986
This theorem is referenced by:  opeq12  4181  opeq2i  4183  opeq2d  4186  oteq2  4189  oteq3  4190  breq2  4419  cbvopab2  4487  cbvopab2v  4490  opthg  4690  eqvinop  4699  opelopabsb  4724  dfid3  4768  opelxp  4882  opabid2  4982  elrn2g  5043  opeldm  5056  elrn2  5092  opelresg  5130  iss  5170  elimasng  5212  issref  5231  dmsnopg  5325  cnvsng  5340  funopg  5632  f1osng  5875  f1oprswap  5876  tz6.12f  5905  fvn0ssdmfun  6035  fsn  6084  fsng  6086  fprg  6096  fvsng  6121  oveq2  6322  cbvoprab2  6390  ovg  6461  elxp4  6763  elxp5  6764  opabex3d  6797  opabex3  6798  op1stg  6831  op2ndg  6832  op1steq  6861  dfoprab4f  6877  seqomlem2  7193  omeu  7311  oeeui  7328  ralxpmap  7546  elixpsn  7586  ixpsnf1o  7587  mapsnen  7672  xpsnen  7681  xpassen  7691  xpf1o  7759  unxpdomlem1  7801  axdc4lem  8910  nqereu  9379  mulcanenq  9410  elreal  9580  ax1rid  9610  fseq1p1m1  11896  swrdccatin1  12875  swrdccat3blem  12887  swrdccatid  12889  swrdccatin12d  12893  wrdlen2  13068  ruclem1  14331  imasaddfnlem  15482  imasvscafn  15491  catidex  15628  catpropd  15662  funcsetcestrclem1  16087  symg2bas  17087  psgnunilem5  17183  efgi  17417  gsumcom2  17655  mat1rhmval  19552  mat1ric  19560  txkgen  20715  cnmpt21  20734  xkoinjcn  20750  txcon  20752  xpstopnlem1  20872  qustgplem  21183  metustid  21617  axlowdim2  25038  axlowdim  25039  axcontlem2  25043  axcontlem3  25044  axcontlem4  25045  axcontlem9  25050  axcontlem10  25051  axcontlem11  25052  1pthoncl  25370  2pthoncl  25381  wwlknextbi  25501  wwlkextinj  25506  wwlkextsur  25507  clwwlkfo  25573  0eusgraiff0rgra  25715  drngoi  26183  isdivrngo  26207  vcoprne  26246  isnvlem  26277  br8d  28266  prsdm  28768  eulerpartlemgvv  29257  bnj941  29632  bnj944  29797  cvmlift2lem1  30073  cvmlift2lem12  30085  br8  30444  br6  30445  br4  30446  fprb  30461  br1steqg  30464  br2ndeqg  30465  dfrn5  30467  elima4  30469  pprodss4v  30699  brimg  30752  brapply  30753  brsuccf  30756  brrestrict  30764  dfrdg4  30766  cgrtriv  30817  brofs  30820  segconeu  30826  btwntriv2  30827  transportprops  30849  brifs  30858  ifscgr  30859  brcgr3  30861  cgrxfr  30870  brcolinear2  30873  colineardim1  30876  brfs  30894  idinside  30899  btwnconn1lem7  30908  btwnconn1lem11  30912  btwnconn1lem12  30913  btwnconn1lem14  30915  brsegle  30923  seglerflx  30927  seglemin  30928  segleantisym  30930  btwnsegle  30932  outsideofeu  30946  outsidele  30947  linedegen  30958  fvline  30959  finxpreclem6  31832  finxpsuclem  31833  poimirlem4  31988  poimirlem26  32010  dibelval3  34759  diblsmopel  34783  dihjatcclem4  35033  dfhe3  36414  dffrege115  36618  dropab2  36844  relopabVD  37337  projf1o  37511  mapsnend  37517  sge0xp  38308  hoidmv1le  38453  pfxval  38963  funsneqopsn  39064  cusgrexg  39557  rgrusgrprc  39653
  Copyright terms: Public domain W3C validator