Theorem opeq1 2541

Description: Equality theorem for ordered pairs.

Assertion

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

Proof of Theorem opeq1

Step	Hyp	Ref	Expression
1		preq1 2500	. . . 4 |- (A = B -> {A, C} = {B, C})
2		preq2 2501	. . . 4 |- ({A, C} = {B, C} -> {{A}, {A, C}} = {{A}, {B, C}})
3	1, 2	syl 10	. . 3 |- (A = B -> {{A}, {A, C}} = {{A}, {B, C}})
4		sneq 2469	. . . 4 |- (A = B -> {A} = {B})
5		preq1 2500	. . . 4 |- ({A} = {B} -> {{A}, {B, C}} = {{B}, {B, C}})
6	4, 5	syl 10	. . 3 |- (A = B -> {{A}, {B, C}} = {{B}, {B, C}})
7	3, 6	eqtrd 1554	. 2 |- (A = B -> {{A}, {A, C}} = {{B}, {B, C}})
8		df-op 2468	. 2 |- <.A, C>. = {{A}, {A, C}}
9		df-op 2468	. 2 |- <.B, C>. = {{B}, {B, C}}
10	7, 8, 9	3eqtr4g 1578	1 |- (A = B -> <.A, C>. = <.B, C>.)

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

This theorem is referenced by:  opeq12 2543  opeq1i 2544  opeq1d 2547  breq1 2677  cbvopab1 2729  cbvopab1s 2730  opth 2843  opthgg 2845  eqvinop 2847  opprc1b 2852  opth2 2856  opabid 2866  opelxp 3271  opabid2 3324  opelcog 3347  dfdmf 3363  eldm2g 3366  dfrnf 3405  elimasn 3483  elimasng 3484  cnvopab 3502  elxp4 3510  elxp5 3511  funopg 3604  fcoi1 3702  dmfco 3830  fvco 3831  fvopabn 3843  fvopab5 3850  fvelrn 3869  funfvima3 3911  tfrlem10 3978  tfrlem11 3979  rdglem2 3996  opreq1 4026  dfoprab2 4049  op1stg 4145  op2ndg 4146  2ndconst 4155  dfec2 4322  fundmen 4489  xpsnen 4498  xpassen 4504  aceq5lem1 4797  aceq5lem4 4800  ltexpq 5145  prlem934a 5202  suppsr 5287  suppsr2 5288  supre 5325  pre-axsup 5356  dffsum 7088  dfisum 7281  isnvlem 8313  nvi 8317  isded 10751  dedi 10752  cmppfd 10760  iscat 10769  cati 10770  imonclem 10823

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