Theorem opeq1 3158

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 3098	. . . 4 |- (A = B -> {A, C} = {B, C})
2		preq2 3099	. . . 4 |- ({A, C} = {B, C} -> {{A}, {A, C}} = {{A}, {B, C}})
3	1, 2	syl 12	. . 3 |- (A = B -> {{A}, {A, C}} = {{A}, {B, C}})
4		sneq 3054	. . . 4 |- (A = B -> {A} = {B})
5		preq1 3098	. . . 4 |- ({A} = {B} -> {{A}, {B, C}} = {{B}, {B, C}})
6	4, 5	syl 12	. . 3 |- (A = B -> {{A}, {B, C}} = {{B}, {B, C}})
7	3, 6	eqtrd 1925	. 2 |- (A = B -> {{A}, {A, C}} = {{B}, {B, C}})
8		df-op 3053	. 2 |- <.A, C>. = {{A}, {A, C}}
9		df-op 3053	. 2 |- <.B, C>. = {{B}, {B, C}}
10	7, 8, 9	3eqtr4g 1953	1 |- (A = B -> <.A, C>. = <.B, C>.)

Syntax hints:   -> wi 3   = wceq 1298  {csn 3044  {cpr 3045  <.cop 3046

This theorem is referenced by:  opeq12 3160  opeq1i 3161  opeq1d 3164  breq1 3341  cbvopab1 3405  cbvopab1s 3406  opth 3532  opthgg 3534  eqvinop 3536  opprc1b 3542  opth2 3546  opabidOLD 3558  opelxpOLD 4037  elvvv 4054  opabid2 4107  opelco2g 4133  dfdmf 4152  eldm2g 4155  dfrnf 4195  elimasnOLD 4290  elimasng 4291  cnvopabOLD 4318  dmsnop 4367  elxp4 4379  elxp5 4380  funopg 4454  funsng 4465  fcoi1OLD 4585  dmfco 4735  fvco 4736  fvopabn 4749  fvopab5 4756  fvelrn 4785  funfvima3 4830  opreq1 4889  dfoprab2 4917  cbvoprab1 4924  cbvoprab1OLD 4925  op1stg 5028  op2ndg 5029  fsplit 5086  tfrlem10 5128  tfrlem11 5129  rdglem2 5146  dfec2 5321  fundmen 5487  xpsnen 5494  xpassen 5500  hartog 5693  aceq5lem1 5897  aceq5lem4 5900  ltexpq 6232  prlem934a 6289  suppsr 6374  suppsr2 6375  supre 6412  pre-axsup 6444  dffsum 8258  dfisum 8452  ssga 9455  gapmlem 9461  gapm 9462  drngi 9493  isnvlem 9561  nvi 9565  oprabopabf 10157  issubsplem1 10246  stoig 10251  fora2 10407  isdivrng 10417  bnj148 12481  elsnres 13825  frxp 13951  prj1 14395  dffprod 14670  subsp2 14902  isded 15083  dedi 15084  cmppfd 15092  dmrngcmp 15098  iscat 15101  cati 15102  imonclem 15162  isseg2 15305  hartogOLD 15384  filnetlem1 15640  filnetlem2 15641  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  prfOLD 15680  opabex3 15701  fsumltisum 15824  fsumleisum 15827  iserzshft2 15829  phtpycolem3 16053  phtpycolem4 16054  dropab1 16424

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-un 2600  df-sn 3049  df-pr 3050  df-op 3053

Copyright terms: Public domain