Theorem dmeq 4955

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 4954	. . 3 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)
2		dmss 4954	. . 3 ⊢ (𝐵 ⊆ 𝐴 → dom 𝐵 ⊆ dom 𝐴)
3	1, 2	anim12i 338	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (dom 𝐴 ⊆ dom 𝐵 ∧ dom 𝐵 ⊆ dom 𝐴))
4		eqss 3252	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3252	. 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 3210  dom cdm 4748

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 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2814  df-un 3214  df-in 3216  df-ss 3223  df-sn 3694  df-pr 3695  df-op 3697  df-br 4109  df-dm 4758

This theorem is referenced by:  dmeqi  4956  dmeqd  4957  xpid11  4979  sqxpeq0  5185  fneq1  5443  eqfnfv2  5775  funopdmsn  5863  offval  6273  ofrfval  6274  offval3  6326  suppval  6436  smoeq  6520  tfrlemi14d  6563  tfr1onlemres  6579  tfrcllemres  6592  rdgivallem  6611  rdgon  6616  rdg0  6617  frec0g  6627  freccllem  6632  frecfcllem  6634  frecsuclem  6636  frecsuc  6637  ereq1  6773  fundmeng  7047  acfun  7513  ccfunen  7577  fundm2domnop0  11216  ennnfonelemj0  13144  ennnfonelemg  13146  ennnfonelemp1  13149  ennnfonelemom  13151  ennnfonelemnn0  13165  ptex  13469  prdsex  13474  blfvalps  15242  reldvg  15536  uhgr0e  16069  incistruhgr  16077  ausgrusgrien  16158  egrsubgr  16250  vtxdgfval  16275  gfsumval  16853