Theorem opeq2 2542

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 2501	. . 3 |- (A = B -> {C, A} = {C, B})
2		preq2 2501	. . 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 2468	. 2 |- <.C, A>. = {{C}, {C, A}}
5		df-op 2468	. 2 |- <.C, B>. = {{C}, {C, B}}
6	3, 4, 5	3eqtr4g 1578	1 |- (A = B -> <.C, A>. = <.C, B>.)

Syntax hints:   -> wi 3   = wceq 997  {csn 2461  {cpr 2462  <.cop 2463

This theorem is referenced by:  opeq12 2543  opeq2i 2545  opeq2d 2548  breq2 2678  cbvopab2v 2732  opthg 2844  opthgg 2845  eqvinop 2847  moop2 2857  opabid 2866  dfid3 2892  opelxpg 3273  opabid2 3324  opelcog 3347  dfdmf 3363  opeldm 3371  dfrnf 3405  elrn2 3406  opelresg 3431  iss 3454  elimasng 3484  intirr 3498  cnvopab 3502  elxp4 3510  elxp5 3511  funopg 3604  fnopabg 3672  fcoi2 3703  tz6.12f 3795  funopfvg 3809  funfvop 3860  fsn 3891  tfrlem11 3979  opreq2 4027  op2ndg 4146  2ndconst 4155  mapsnen 4490  xpsnen 4498  xpassen 4504  aceq3lem 4794  elreal 5315  seq1val 6571  dfseq0 6652  vcoprne 8282  isnvlem 8313  nvi 8317  ref3w 10566  isded 10751  dedi 10752  cmppfd 10760  iscat 10769  cati 10770  iepiclem 10833

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-v 1859  df-un 2101  df-sn 2464  df-pr 2465  df-op 2468

Copyright terms: Public domain