Theorem opeq1 3345

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		sneq 3247	. . 3 |- (A = B -> {A} = {B})
2		preq1 3288	. . 3 |- (A = B -> {A, C} = {B, C})
3	1, 2	preq12d 3296	. 2 |- (A = B -> {{A}, {A, C}} = {{B}, {B, C}})
4		df-op 3246	. 2 |- <.A, C>. = {{A}, {A, C}}
5		df-op 3246	. 2 |- <.B, C>. = {{B}, {B, C}}
6	3, 4, 5	3eqtr4g 2201	1 |- (A = B -> <.A, C>. = <.B, C>.)

Syntax hints:   -> wi 3   = wceq 1586  {csn 3238  {cpr 3239  <.cop 3240

This theorem is referenced by:  opeq12 3347  opeq1i 3348  opeq1d 3351  breq1 3510  cbvopab1 3573  cbvopab1s 3574  opth 3695  opthgg 3697  eqvinop 3699  opprc1b 3705  opth2 3709  elvvv 4187  opabid2 4237  opelco2g 4261  dfdmf 4278  eldm2g 4281  dfrnf 4316  elsnres 4369  elimasng 4409  dmsnop 4472  elxp4 4482  elxp5 4483  funopg 4556  funsng 4566  f1osng 4760  dmfco 4821  fvco 4822  fvopabn 4835  fvopab5 4842  fvsng 4845  fvelrn 4875  fsng 4902  funfvima3 4922  opabex3 4933  opreq1 4986  oprabid 5002  dfoprab2 5012  cbvoprab1 5019  op1stg 5134  op2ndg 5135  oprabopabf 5170  fsplit 5209  frxp 5210  tfrlem10 5292  tfrlem11 5293  rdglem2 5310  omeu 5426  dfec2 5482  fundmen 5648  xpsnen 5658  xpassen 5664  unxpdomlem1 5817  aceq5lem1 6189  aceq5lem4 6192  fodomnumlem 6208  axdc4lem 6310  ltexpq 6598  prlem934a 6655  suppsr 6740  suppsr2 6741  supre 6778  pre-axsup 6807  dffsum 8654  dfisum 8848  ssga 10324  gapmlem 10330  gapm 10331  drngi 10362  isnvlem 10430  nvi 10434  subsp 11080  issubsplem1 11082  stoigOLD 11088  stoig 11089  fora2 11245  isdivrngo 11255  bnj148 13261  elsnresOLD 14455  frxpOLD 14604  elfuns 14774  prj1b 15105  prj3 15106  dffprod 15409  subsp2OLD 15664  ttcn2 15678  isded 15877  dedi 15878  cmppfd 15886  dmrngcmp 15892  iscat 15895  cati 15896  imonclem 15956  isseg2 16115  hartog 16208  filnetlem1 16464  filnetlem2 16465  filnetlem3 16466  filnetlem4 16467  filnetlem5 16468  prfOLD 16504  opabex3OLD 16525  fsumltisum 16648  fsumleisum 16651  iserzshft2 16653  phtpycolem3 16877  phtpycolem4 16878  dropab1 17248

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-v 2540  df-un 2832  df-sn 3242  df-pr 3243  df-op 3246

Copyright terms: Public domain