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

Theorem opeq1 3797
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 2344 . . . 4  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 687 . . 3  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3652 . . . 4  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3707 . . . 4  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3715 . . 3  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
6 eqidd 2285 . . 3  |-  ( A  =  B  ->  (/)  =  (/) )
72, 5, 6ifbieq12d 3588 . 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 3794 . 2  |-  <. A ,  C >.  =  if ( ( A  e.  _V  /\  C  e.  _V ) ,  { { A } ,  { A ,  C } } ,  (/) )
9 dfopif 3794 . 2  |-  <. B ,  C >.  =  if ( ( B  e.  _V  /\  C  e.  _V ) ,  { { B } ,  { B ,  C } } ,  (/) )
107, 8, 93eqtr4g 2341 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   _Vcvv 2789   (/)c0 3456   ifcif 3566   {csn 3641   {cpr 3642   <.cop 3644
This theorem is referenced by:  opeq12  3799  opeq1i  3800  opeq1d  3803  oteq1  3806  breq1  4027  cbvopab1  4090  cbvopab1s  4092  opthg  4245  eqvinop  4250  opelopabsb  4274  opelxp  4718  elvvv  4748  opabid2  4814  opeliunxp2  4823  elsnres  4990  elimasng  5038  dmsnopg  5142  cnvsng  5156  elxp4  5158  elxp5  5159  funopg  5252  f1osng  5479  f1oprswap  5480  dmfco  5554  fvelrn  5622  fsng  5658  fvsng  5675  funfvima3  5716  opabex3  5730  oveq1  5826  oprabid  5843  dfoprab2  5856  cbvoprab1  5879  op1stg  6093  op2ndg  6094  dfoprab4f  6139  frxp  6186  tfrlem11  6399  omeu  6578  oeeui  6595  elixpsn  6850  fundmen  6929  xpsnen  6941  xpassen  6951  xpf1o  7018  unxpdomlem1  7062  dfac5lem1  7745  dfac5lem4  7748  axdc4lem  8076  nqereu  8548  mulcanenq  8579  archnq  8599  prlem934  8652  supsrlem  8728  supsr  8729  fsum2dlem  12227  vdwlem10  13031  imasaddfnlem  13424  catideu  13571  iscatd2  13577  catlid  13579  catpropd  13606  efgmval  15015  efgi  15022  vrgpval  15070  gsumcom2  15220  txkgen  17340  cnmpt21  17359  xkoinjcn  17375  txcon  17377  pt1hmeo  17491  divstgplem  17797  dvbsss  19246  drngoi  21066  isdivrngo  21090  isnvlem  21158  br8  23516  br6  23517  br4  23518  dfdm5  23533  elfuns  23861  brimg  23883  brapply  23884  brrestrict  23894  dfrdg4  23895  axlowdim2  23995  axlowdim  23996  axcontlem10  24008  axcontlem12  24010  cgrdegen  24034  brofs  24035  cgrextend  24038  brifs  24073  ifscgr  24074  brcgr3  24076  brcolinear2  24088  colineardim1  24091  brfs  24109  idinside  24114  btwnconn1lem7  24123  btwnconn1lem11  24127  btwnconn1lem12  24128  brsegle  24138  outsideofeu  24161  fvray  24171  linedegen  24173  fvline  24174  eqvinopb  24363  prj1b  24477  prj3  24478  fprg  24532  isded  25135  dedi  25136  cmppfd  25144  dmrngcmp  25150  iscatOLD  25153  cati  25154  imonclem  25212  dropab1  27049  relopabVD  27945  dicelval3  30637  dihjatcclem4  30878
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650
  Copyright terms: Public domain W3C validator