Theorem opeq2 3159

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 3099	. . 3 |- (A = B -> {C, A} = {C, B})
2		preq2 3099	. . 3 |- ({C, A} = {C, B} -> {{C}, {C, A}} = {{C}, {C, B}})
3	1, 2	syl 12	. 2 |- (A = B -> {{C}, {C, A}} = {{C}, {C, B}})
4		df-op 3053	. 2 |- <.C, A>. = {{C}, {C, A}}
5		df-op 3053	. 2 |- <.C, B>. = {{C}, {C, B}}
6	3, 4, 5	3eqtr4g 1953	1 |- (A = B -> <.C, A>. = <.C, B>.)

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

This theorem is referenced by:  opeq12 3160  opeq2i 3162  opeq2d 3165  breq2 3342  cbvopab2v 3408  opthg 3533  opthgg 3534  eqvinop 3536  moop2 3548  opabidOLD 3558  dfid3 3587  opelxpg 4039  opabid2 4107  opelco2g 4133  dfdmf 4152  opeldm 4160  dfrnf 4195  elrn2 4196  opelresg 4224  iss 4254  issOLD 4255  elimasng 4291  intirrOLD 4313  cnvopabOLD 4318  dmsnop 4367  elxp4 4379  elxp5 4380  funopg 4454  funsng 4465  iunfopab 4542  fnopabg 4546  fcoi2OLD 4587  tz6.12f 4695  funopfvg 4711  funfvop 4776  fsn 4807  opreq2 4890  op2ndg 5029  fsplit 5086  tfrlem11 5129  mapsnen 5488  xpsnen 5494  xpassen 5500  aceq3lem 5894  elreal 6402  seq1val 7725  dfseq0 7806  drngi 9493  vcoprne 9530  isnvlem 9561  nvi 9565  oprabopabf 10157  issubspt 10247  stoig 10251  isdivrng 10417  bnj147 12480  bnj519 12520  bnj941 12842  bnj939 13338  elrn2g 13877  ref4w 14370  prj1 14395  repcpwti 14503  cbcpcp 14504  prodeq3 14663  subsp2 14902  subspemp2 14904  ttcn 14913  isded 15083  dedi 15084  cmppfd 15092  dmrngcmp 15098  iscat 15101  cati 15102  iepiclem 15172  isseg2 15305  filnetlem1 15640  filnetlem2 15641  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  prfOLD 15680  opabex3 15701  oprabvalg 15706  cbvoprab2 15708  seqz1g 15806  seqzp1g 15807  seq1seqzg 15808  dropab2 16425  islvec 17188

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