Theorem dmeq 4812

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 4811	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 4811	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 336	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3163	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3163	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 200	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1349   C_ wss 3122   dom cdm 4612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-v 2733  df-un 3126  df-in 3128  df-ss 3135  df-sn 3590  df-pr 3591  df-op 3593  df-br 3991  df-dm 4622

This theorem is referenced by:  dmeqi  4813  dmeqd  4814  xpid11  4835  sqxpeq0  5036  fneq1  5288  eqfnfv2  5598  offval  6072  ofrfval  6073  offval3  6117  smoeq  6273  tfrlemi14d  6316  tfr1onlemres  6332  tfrcllemres  6345  rdgivallem  6364  rdgon  6369  rdg0  6370  frec0g  6380  freccllem  6385  frecfcllem  6387  frecsuclem  6389  frecsuc  6390  ereq1  6524  fundmeng  6789  acfun  7188  ccfunen  7230  ennnfonelemj0  12360  ennnfonelemg  12362  ennnfonelemp1  12365  ennnfonelemom  12367  ennnfonelemnn0  12381  blfvalps  13264  reldvg  13527