Theorem dmeq 4879

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 4878	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 4878	. . 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 3208	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3208	. 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 1373   C_ wss 3166   dom cdm 4676

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046  df-dm 4686

This theorem is referenced by:  dmeqi  4880  dmeqd  4881  xpid11  4902  sqxpeq0  5107  fneq1  5363  eqfnfv2  5680  funopdmsn  5766  offval  6168  ofrfval  6169  offval3  6221  smoeq  6378  tfrlemi14d  6421  tfr1onlemres  6437  tfrcllemres  6450  rdgivallem  6469  rdgon  6474  rdg0  6475  frec0g  6485  freccllem  6490  frecfcllem  6492  frecsuclem  6494  frecsuc  6495  ereq1  6629  fundmeng  6901  acfun  7321  ccfunen  7378  fundm2domnop0  10992  ennnfonelemj0  12805  ennnfonelemg  12807  ennnfonelemp1  12810  ennnfonelemom  12812  ennnfonelemnn0  12826  ptex  13129  prdsex  13134  blfvalps  14890  reldvg  15184