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

Theorem opeq1 3952
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )

Proof of Theorem opeq1
StepHypRef Expression
1 eleq1 2472 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 686 . . 3  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3793 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3851 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3859 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2413 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3729 . 2  |-  ( A  =  B  ->  if ( ( A  e. 
_V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) ) )
8 dfopif 3949 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3949 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2469 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   _Vcvv 2924   (/)c0 3596   ifcif 3707   {csn 3782   {cpr 3783   <.cop 3785
This theorem is referenced by:  opeq12  3954  opeq1i  3955  opeq1d  3958  oteq1  3961  breq1  4183  cbvopab1  4246  cbvopab1s  4248  opthg  4404  eqvinop  4409  opelopabsb  4433  opelxp  4875  elvvv  4904  opabid2  4971  opeliunxp2  4980  elsnres  5149  elimasng  5197  dmsnopg  5308  cnvsng  5322  elxp4  5324  elxp5  5325  funopg  5452  f1osng  5683  f1oprswap  5684  dmfco  5764  fvelrn  5833  fsng  5874  fprg  5882  fvsng  5894  funfvima3  5942  opabex3d  5956  opabex3  5957  oveq1  6055  oprabid  6072  dfoprab2  6088  cbvoprab1  6111  op1stg  6326  op2ndg  6327  dfoprab4f  6372  frxp  6423  tfrlem11  6616  omeu  6795  oeeui  6812  elixpsn  7068  fundmen  7147  xpsnen  7159  xpassen  7169  xpf1o  7236  unxpdomlem1  7280  dfac5lem1  7968  dfac5lem4  7971  axdc4lem  8299  nqereu  8770  mulcanenq  8801  archnq  8821  prlem934  8874  supsrlem  8950  supsr  8951  fsum2dlem  12517  vdwlem10  13321  imasaddfnlem  13716  catideu  13863  iscatd2  13869  catlid  13871  catpropd  13898  efgmval  15307  efgi  15314  vrgpval  15362  gsumcom2  15512  txkgen  17645  cnmpt21  17664  xkoinjcn  17680  txcon  17682  pt1hmeo  17799  cnextfvval  18057  divstgplem  18111  dvbsss  19750  drngoi  21956  isdivrngo  21980  isnvlem  22050  fprod2dlem  25265  br8  25335  br6  25336  br4  25337  eldm3  25341  dfdm5  25354  brimg  25698  brapply  25699  brrestrict  25710  dfrdg4  25711  axlowdim2  25811  axlowdim  25812  axcontlem10  25824  axcontlem12  25826  cgrdegen  25850  brofs  25851  cgrextend  25854  brifs  25889  ifscgr  25890  brcgr3  25892  brcolinear2  25904  colineardim1  25907  brfs  25925  idinside  25930  btwnconn1lem7  25939  btwnconn1lem11  25943  btwnconn1lem12  25944  brsegle  25954  outsideofeu  25977  fvray  25987  linedegen  25989  fvline  25990  dropab1  27525  el2xptp  27956  swrdccatin1  28024  relopabVD  28731  dicelval3  31675  dihjatcclem4  31916
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791
  Copyright terms: Public domain W3C validator