Theorem opeq1 2487

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 2448	. . . 4 |- (A = B -> {A, C} = {B, C})
2		preq2 2449	. . . 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 2417	. . . 4 |- (A = B -> {A} = {B})
5		preq1 2448	. . . 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 1507	. 2 |- (A = B -> {{A}, {A, C}} = {{B}, {B, C}})
8		df-op 2416	. 2 |- <.A, C>. = {{A}, {A, C}}
9		df-op 2416	. 2 |- <.B, C>. = {{B}, {B, C}}
10	7, 8, 9	3eqtr4g 1531	1 |- (A = B -> <.A, C>. = <.B, C>.)

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

This theorem is referenced by:  opeq12 2489  opeq1i 2490  opeq1d 2493  breq1 2622  cbvopab1 2674  cbvopab1s 2675  opth 2787  opthgg 2789  eqvinop 2791  opprc1b 2796  opth2 2800  opabid 2810  opelxp 3214  opabid2 3267  opelcog 3290  dfdmf 3306  eldm2g 3309  dfrnf 3348  elimasn 3426  elimasng 3427  cnvopab 3445  elxp4 3453  elxp5 3454  funopg 3547  fcoi1 3645  dmfco 3773  fvco 3774  fvopabn 3786  fvopab5 3793  fvelrn 3812  funfvima3 3854  tfrlem10 3920  tfrlem11 3921  rdglem2 3938  opreq1 3968  dfoprab2 3991  op1stg 4087  op2ndg 4088  2ndconst 4097  dfec2 4264  fundmen 4428  xpsnen 4435  xpassen 4441  aceq5lem1 4735  aceq5lem4 4738  ltexpq 5080  prlem934a 5137  suppsr 5222  suppsr2 5223  supre 5260  pre-axsup 5291  dffsum 6998  dfisum 7191  isnvlem 8229  nvi 8233  isded 10669  dedi 10670  cmppfd 10678  iscat 10687  cati 10688  imonclem 10741

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