Theorem dmeqi 3312

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 3311	. 2 |- (A = B -> dom A = dom B)
3	1, 2	ax-mp 7	1 |- dom A = dom B

Syntax hints:   = wceq 956  dom cdm 3170

This theorem is referenced by:  dmsnsnsn 3329  dmxp 3332  dmxpin 3334  rncoss 3364  rncoeq 3367  rnsnop 3450  op2nda 3452  rnun 3457  rnin 3458  rnxp 3472  fvopab4ndm 3784  fopab2 3823  tfrlem8 3918  rdgsucopabn 3947  dmoprab 4002  xpassen 4441  sbthlem5 4451  dmaddpi 5018  dmmulpi 5019  dmaddpq 5059  dmmulpq 5061  dmrecpq 5074  genpdm 5105  dmaddsr 5194  dmmulsr 5195  axaddopr 5265  axmulopr 5266  uzssz 6430  infmap2lem1 7579  ismeti 7802  0met 7825  cnmetba 7903  cncfmet 7905  remetba 7909  xplmi 7973  xplmi2 7974  xplm 7975  xpcn 7976  oprcn 7977  bopcnlem3 7983  bopcn 7985  resgrprn 8095  vsfval 8254  dfhnorm2 8988  hhshsslem1 9137  adj1o 9818  dmadjss 9819  ghomfo 10391  hmeogrp 10538  aidm 10683  aidmold 10684  dmo 10709  jdmo 10711  cmpmorp 10712  mrdmcd 10722  homib 10724  cmphmia 10726  cmphmib 10727  iri 10728  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-in 2051  df-ss 2053  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-dm 3188

Copyright terms: Public domain