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

Theorem opeq1 3696
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 2313 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 688 . . 3  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3555 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3610 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3618 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2254 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3492 . 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 3693 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3693 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2310 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2727   (/)c0 3362   ifcif 3470   {csn 3544   {cpr 3545   <.cop 3547
This theorem is referenced by:  opeq12  3698  opeq1i  3699  opeq1d  3702  oteq1  3705  breq1  3923  cbvopab1  3986  cbvopab1s  3988  opthg  4139  eqvinop  4144  opelopabsb  4168  opelxp  4626  elvvv  4656  opabid2  4722  opeliunxp2  4731  elsnres  4898  elimasng  4946  dmsnopg  5050  cnvsng  5064  elxp4  5066  elxp5  5067  funopg  5144  f1osng  5371  f1oprswap  5372  dmfco  5445  fvelrn  5513  fsng  5549  fvsng  5566  funfvima3  5607  opabex3  5621  oveq1  5717  oprabid  5734  dfoprab2  5747  cbvoprab1  5770  op1stg  5984  op2ndg  5985  dfoprab4f  6030  frxp  6077  tfrlem11  6290  omeu  6469  oeeui  6486  elixpsn  6741  fundmen  6819  xpsnen  6831  xpassen  6841  xpf1o  6908  unxpdomlem1  6952  dfac5lem1  7634  dfac5lem4  7637  axdc4lem  7965  nqereu  8433  mulcanenq  8464  archnq  8484  prlem934  8537  supsrlem  8613  supsr  8614  fsum2dlem  12110  vdwlem10  12911  imasaddfnlem  13304  catideu  13421  iscatd2  13427  catlid  13429  catpropd  13456  efgmval  14856  efgi  14863  vrgpval  14911  gsumcom2  15061  txkgen  17178  cnmpt21  17197  xkoinjcn  17213  txcon  17215  pt1hmeo  17329  divstgplem  17635  dvbsss  19084  drngoi  20904  isdivrngo  20928  isnvlem  20996  br8  23283  br6  23284  br4  23285  dfdm5  23300  elfuns  23628  brimg  23650  brapply  23651  brrestrict  23661  dfrdg4  23662  axlowdim2  23762  axlowdim  23763  axcontlem10  23775  axcontlem12  23777  cgrdegen  23801  brofs  23802  cgrextend  23805  brifs  23840  ifscgr  23841  brcgr3  23843  brcolinear2  23855  colineardim1  23858  brfs  23876  idinside  23881  btwnconn1lem7  23890  btwnconn1lem11  23894  btwnconn1lem12  23895  brsegle  23905  outsideofeu  23928  fvray  23938  linedegen  23940  fvline  23941  eqvinopb  24130  prj1b  24244  prj3  24245  fprg  24299  isded  24902  dedi  24903  cmppfd  24911  dmrngcmp  24917  iscatOLD  24920  cati  24921  imonclem  24979  dropab1  26817  relopabVD  27464  dicelval3  30274  dihjatcclem4  30515
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553
  Copyright terms: Public domain W3C validator