Theorem opeq2 2488

Description: Equality theorem for ordered pairs.

Assertion

Ref	Expression
opeq2	|- (A = B -> <.C, A>. = <.C, B>.)

Proof of Theorem opeq2

Step	Hyp	Ref	Expression
1		preq2 2449	. . 3 |- (A = B -> {C, A} = {C, B})
2		preq2 2449	. . 3 |- ({C, A} = {C, B} -> {{C}, {C, A}} = {{C}, {C, B}})
3	1, 2	syl 10	. 2 |- (A = B -> {{C}, {C, A}} = {{C}, {C, B}})
4		df-op 2416	. 2 |- <.C, A>. = {{C}, {C, A}}
5		df-op 2416	. 2 |- <.C, B>. = {{C}, {C, B}}
6	3, 4, 5	3eqtr4g 1531	1 |- (A = B -> <.C, A>. = <.C, B>.)

Syntax hints:   -> wi 3   = wceq 956  {csn 2409  {cpr 2410  <.cop 2411

This theorem is referenced by:  opeq12 2489  opeq2i 2491  opeq2d 2494  breq2 2623  cbvopab2v 2677  opthg 2788  opthgg 2789  eqvinop 2791  moop2 2801  opabid 2810  dfid3 2836  opelxpg 3216  opabid2 3267  opelcog 3290  dfdmf 3306  opeldm 3314  dfrnf 3348  elrn2 3349  opelresg 3374  iss 3397  elimasng 3427  intirr 3441  cnvopab 3445  elxp4 3453  elxp5 3454  funopg 3547  fnopabg 3615  fcoi2 3646  tz6.12f 3738  funopfvg 3752  funfvop 3803  fsn 3834  tfrlem11 3921  opreq2 3969  op2ndg 4088  2ndconst 4097  mapsnen 4429  xpsnen 4435  xpassen 4441  aceq3lem 4732  elreal 5250  seq1val 6312  dfseq0 6563  vcoprne 8198  isnvlem 8229  nvi 8233  isded 10669  dedi 10670  cmppfd 10678  iscat 10687  cati 10688

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416

Copyright terms: Public domain