Theorem opeq2 2553

Description: Equality theorem for ordered pairs.

Assertion

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

Proof of Theorem opeq2

Step	Hyp	Ref	Expression
1		preq2 2510	. . 3 |- (A = B -> {C, A} = {C, B})
2		preq2 2510	. . 3 |- ({C, A} = {C, B} -> {{C}, {C, A}} = {{C}, {C, B}})
3	1, 2	syl 10	. 2 |- (A = B -> {{C}, {C, A}} = {{C}, {C, B}})
4		df-op 2474	. 2 |- <.C, A>. = {{C}, {C, A}}
5		df-op 2474	. 2 |- <.C, B>. = {{C}, {C, B}}
6	3, 4, 5	3eqtr4g 1574	1 |- (A = B -> <.C, A>. = <.C, B>.)

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

This theorem is referenced by:  opeq12 2554  opeq2i 2556  opeq2d 2559  breq2 2696  cbvopab2v 2751  opthg 2864  opthgg 2865  eqvinop 2867  moop2 2878  opabid 2887  dfid3 2914  opelxpg 3299  opabid2 3360  opelco2g 3380  dfdmf 3397  opeldm 3405  dfrnf 3435  elrn2 3436  opelresg 3461  iss 3487  elimasng 3519  intirr 3533  cnvopab 3537  elxp4 3585  elxp5 3586  funopg 3652  fnopabg 3722  fcoi2 3753  tz6.12f 3849  funopfvg 3863  funfvop 3917  fsn 3948  opreq2 4027  op2ndg 4149  fsplit 4204  tfrlem11 4222  mapsnen 4570  xpsnen 4576  xpassen 4582  aceq3lem 4878  elreal 5404  seq1val 6677  dfseq0 6758  drngi 8408  vcoprne 8445  isnvlem 8476  nvi 8480  ref3w 10772  prj1 10809  isdivrng 10968  issubspt 11059  subspemp2 11061  stoig 11064  isded 11190  dedi 11191  cmppfd 11199  dmrngcmp 11205  iscat 11208  cati 11209  iepiclem 11278  filnetlem1 11763  filnetlem2 11764  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  opabex3 11806  oprabopabf 11807

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