Theorem dmeqd 2533

Description: Equality deduction for domain.

Hypothesis

Ref	Expression
dmeqd.1	|- (ph -> A = B)

Assertion

Ref	Expression
dmeqd	|- (ph -> dom A = dom B)

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 |- (ph -> A = B)
2		dmeq 2531	. 2 |- (A = B -> dom A = dom B)
3	1, 2	syl 12	1 |- (ph -> dom A = dom B)

Syntax hints:   -> wi 2   = wceq 1091  dom cdm 2410

This theorem is referenced by:  dmsnop 2547  dmxpid 2553  rneq 2555  elxp4 2640  tfrlem10 2958  1stval 3089  fo1st 3094  f1stres 3096  xpassen 3344  xpdom2 3345  xpmapenlem2 3392  xpmapenlem4 3394  xpmapenlem5 3395

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