Theorem dmeqi 2532

Description: Equality inference for domain.

Hypothesis

Ref	Expression
dmeqi.1	⊢ A = B

Assertion

Ref	Expression
dmeqi	⊢ dom A = dom B

Proof of Theorem dmeqi

Step	Hyp	Ref	Expression
1		dmeqi.1	. 2 ⊢ A = B
2		dmeq 2531	. 2 ⊢ (A = B → dom A = dom B)
3	1, 2	ax-mp 6	1 ⊢ dom A = dom B

Syntax hints:   = wceq 1091  dom cdm 2410

This theorem is referenced by:  dmsnsnsn 2548  dmxp 2552  rnco 2571  rncoeq 2574  rnsnop 2637  op2nda 2639  rnun 2644  rnin 2645  rnxp 2657  fconst 2774  fopab2 2891  tfrlem10 2958  rdgsucopabn 2985  dmoprab 3031  xpassen 3344  sbthlem5 3353  dmaddpi 3812  dmmulpi 3813  dmaddpq 3853  dmmulpq 3855  dmrecpq 3868  genpdm 3899  dmaddsr 3988  dmmulsr 3989  infmap2lem1 4951

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-in 1491  df-ss 1492  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-dm 2428

metamath.org