Theorem dmeq 4956

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

Assertion

Ref	Expression
dmeq	|- ( A = B -> dom A = dom B )

Proof of Theorem dmeq

Step	Hyp	Ref	Expression
1		dmss 4955	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 4955	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 338	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3253	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3253	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 201	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1398   C_ wss 3211   dom cdm 4749

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 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110  df-dm 4759

This theorem is referenced by:  dmeqi  4957  dmeqd  4958  xpid11  4980  sqxpeq0  5186  fneq1  5444  eqfnfv2  5776  funopdmsn  5864  offval  6274  ofrfval  6275  offval3  6327  suppval  6437  smoeq  6521  tfrlemi14d  6564  tfr1onlemres  6580  tfrcllemres  6593  rdgivallem  6612  rdgon  6617  rdg0  6618  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  ereq1  6774  fundmeng  7048  acfun  7514  ccfunen  7578  fundm2domnop0  11220  ennnfonelemj0  13152  ennnfonelemg  13154  ennnfonelemp1  13157  ennnfonelemom  13159  ennnfonelemnn0  13173  ptex  13477  prdsex  13482  blfvalps  15250  reldvg  15544  uhgr0e  16077  incistruhgr  16085  ausgrusgrien  16166  egrsubgr  16258  vtxdgfval  16283  gfsumval  16862