Theorem opeq1 2552

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 2509	. . . 4 |- (A = B -> {A, C} = {B, C})
2		preq2 2510	. . . 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 2475	. . . 4 |- (A = B -> {A} = {B})
5		preq1 2509	. . . 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 1550	. 2 |- (A = B -> {{A}, {A, C}} = {{B}, {B, C}})
8		df-op 2474	. 2 |- <.A, C>. = {{A}, {A, C}}
9		df-op 2474	. 2 |- <.B, C>. = {{B}, {B, C}}
10	7, 8, 9	3eqtr4g 1574	1 |- (A = B -> <.A, C>. = <.B, C>.)

Syntax hints:   -> wi 3   = wceq 992  {csn 2467  {cpr 2468  <.cop 2469

This theorem is referenced by:  opeq12 2554  opeq1i 2555  opeq1d 2558  breq1 2695  cbvopab1 2748  cbvopab1s 2749  opth 2863  opthgg 2865  eqvinop 2867  opprc1b 2872  opth2 2876  opabid 2887  opelxp 3297  elvvv 3314  opabid2 3360  opelco2g 3380  dfdmf 3397  eldm2g 3400  dfrnf 3435  elimasn 3518  elimasng 3519  cnvopab 3537  elxp4 3585  elxp5 3586  funopg 3652  fcoi1 3752  dmfco 3884  fvco 3885  fvopabn 3897  fvopab5 3904  fvelrn 3926  funfvima3 3968  opreq1 4026  dfoprab2 4050  cbvoprab1 4057  op1stg 4148  op2ndg 4149  fsplit 4204  tfrlem10 4221  tfrlem11 4222  rdglem2 4239  dfec2 4404  fundmen 4569  xpsnen 4576  xpassen 4582  aceq5lem1 4881  aceq5lem4 4884  ltexpq 5234  prlem934a 5291  suppsr 5376  suppsr2 5377  supre 5414  pre-axsup 5445  dffsum 7201  dfisum 7395  drngi 8408  isnvlem 8476  nvi 8480  prj1 10809  fora2 10953  isdivrng 10968  issubsplem1 11058  stoig 11064  isded 11190  dedi 11191  cmppfd 11199  dmrngcmp 11205  iscat 11208  cati 11209  imonclem 11268  hartog 11436  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  ssga 11777  gapmlem 11783  gapm 11784  opabex3 11806  oprabopabf 11807  fsumltisum 11887  fsumleisum 11890  iserzshft2 11892  phtpycolem3 12095  phtpycolem4 12096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-sn 2470  df-pr 2471  df-op 2474

Copyright terms: Public domain