Theorem dmeqd 4889

Description: Equality deduction for domain. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
dmeqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
dmeqd	⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeqd

Step	Hyp	Ref	Expression
1		dmeqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dmeq 4887	. 2 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   = wceq 1373  dom cdm 4683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-sn 3644  df-pr 3645  df-op 3647  df-br 4052  df-dm 4693

This theorem is referenced by:  rneq  4914  dmsnsnsng  5169  elxp4  5179  f10d  5569  fndmin  5700  1stvalg  6241  fo1st  6256  f1stres  6258  errn  6655  xpassen  6940  xpdom2  6941  frecuzrdgtclt  10588  s1dmg  11102  swrdval  11124  swrd0g  11136  shftdm  11208  ennnfonelemg  12849  ennnfonelem1  12853  ennnfonelemhdmp1  12855  ennnfonelemkh  12858  ennnfonelemhf1o  12859  ennnfonelemex  12860  ennnfonelemhom  12861  isstruct2im  12917  isstruct2r  12918  setsvalg  12937  prdsval  13180  igsumvalx  13296  cnprcl2k  14753  psmetdmdm  14871  xmetdmdm  14903  blfvalps  14932  limccl  15206  ellimc3apf  15207  dvfvalap  15228  dvcj  15256  dvexp  15258  dvmptclx  15265  dvmptaddx  15266  dvmptmulx  15267  isuhgrm  15742  isushgrm  15743  uhgreq12g  15747  isuhgropm  15752  uhgrun  15757  isupgren  15766  upgrop  15775  isumgren  15776  upgr1edc  15789  upgrun  15792  umgrun  15794