Theorem opeq1 1876

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 1870	. . . 4 ⊢ (A = B → {A, C} = {B, C})
2		preq2 1871	. . . 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 1816	. . . 4 ⊢ (A = B → {A} = {B})
5		preq1 1870	. . . 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 1128	. 2 ⊢ (A = B → {{A}, {A, C}} = {{B}, {B, C}})
8		df-op 1815	. 2 ⊢ ⟨A, C⟩ = {{A}, {A, C}}
9		df-op 1815	. 2 ⊢ ⟨B, C⟩ = {{B}, {B, C}}
10	7, 8, 9	3eqtr4g 1147	1 ⊢ (A = B → ⟨A, C⟩ = ⟨B, C⟩)

Syntax hints:   → wi 2   = wceq 1091  {csn 1808  {cpr 1809  ⟨cop 1810

This theorem is referenced by:  opeq12 1878  opth 1898  eqvinop 1901  opprc1b 1906  opth2 1909  moop2 1910  breq1 2065  opabid 2099  cbvopab1 2106  cbvopab1s 2107  cbvopab1v 2108  opelxp 2452  opelcog 2511  dfdmf 2526  eldmg 2529  dfrnf 2561  imasn 2616  elimasn 2617  cnvopab 2632  elxp4 2640  elxp5 2641  fcoi1 2765  dmfco 2864  fvco 2865  fvopabn 2873  fvrn 2888  funfvima3 2906  tfrlem10 2958  tfrlem11 2959  rdglem2 2976  opreq1 3006  dfoprab2 3021  cbvoprab12 3028  elrnoprab 3054  ec2 3203  fundmen 3333  xpsnen 3339  xpassen 3344  xpmapenlem2 3392  aceq5lem1 3558  aceq5lem4 3561  ltexpq 3874  halfpq 3876  prlem934a 3931  suppsr 4016  suppsr2 4017  supre 4054  axsup 4088

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815

metamath.org