Theorem dmeq 4961

Description: Equality theorem for domain. (Contributed by NM, 11-Aug-1994.)

Assertion

Ref	Expression
dmeq	⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Proof of Theorem dmeq

Step	Hyp	Ref	Expression
1		dmss 4960	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 4960	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 338	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3257	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3257	. 2 ⊢ (dom 𝐴 = dom 𝐵 ↔ (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
6	3, 4, 5	3imtr4i 201	1 ⊢ (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ⊆ wss 3214  dom cdm 4754

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-in 3220  df-ss 3227  df-sn 3700  df-pr 3701  df-op 3703  df-br 4115  df-dm 4764

This theorem is referenced by:  dmeqi  4962  dmeqd  4963  xpid11  4985  sqxpeq0  5191  fneq1  5449  eqfnfv2  5781  funopdmsn  5869  offval  6283  ofrfval  6284  offval3  6340  suppval  6450  smoeq  6534  tfrlemi14d  6577  tfr1onlemres  6593  tfrcllemres  6606  rdgivallem  6625  rdgon  6630  rdg0  6631  frec0g  6641  freccllem  6646  frecfcllem  6648  frecsuclem  6650  frecsuc  6651  ereq1  6787  fundmeng  7061  acfun  7527  ccfunen  7594  fundm2domnop0  11248  ennnfonelemj0  13240  ennnfonelemg  13242  ennnfonelemp1  13245  ennnfonelemom  13247  ennnfonelemnn0  13261  ptex  13565  gfsumval  14106  prdsex  14118  blfvalps  15380  reldvg  15674  uhgr0e  16207  incistruhgr  16215  ausgrusgrien  16296  egrsubgr  16388  vtxdgfval  16413