Theorem dmeq 5192

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 5191	. . 3 |- ( A C_ B -> dom A C_ dom B )
2		dmss 5191	. . 3 |- ( B C_ A -> dom B C_ dom A )
3	1, 2	anim12i 564	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( dom A C_ dom B /\ dom B C_ dom A ) )
4		eqss 3504	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		eqss 3504	. 2 |- ( dom A = dom B <-> ( dom A C_ dom B /\ dom B C_ dom A ) )
6	3, 4, 5	3imtr4i 266	1 |- ( A = B -> dom A = dom B )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1398   C_ wss 3461   dom cdm 4988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-dm 4998

This theorem is referenced by:  dmeqi  5193  dmeqd  5194  xpid11  5213  fneq1  5651  eqfnfv2  5958  nvof1o  6161  offval  6520  ofrfval  6521  offval3  6767  suppval  6893  smoeq  7013  tz7.44lem1  7063  tz7.44-2  7065  tz7.44-3  7066  ereq1  7310  fundmeng  7583  fseqenlem2  8397  dfac3  8493  dfac9  8507  dfac12lem1  8514  dfac12r  8517  ackbij2lem2  8611  ackbij2lem3  8612  r1om  8615  cfsmolem  8641  cfsmo  8642  dcomex  8818  axdc2lem  8819  axdc3lem2  8822  axdc3lem4  8824  ac7g  8845  ttukey2g  8887  s4dom  12858  relexp0g  12939  relexpsucnnr  12942  dfrtrcl2  12977  ello1  13420  elo1  13431  isoval  15253  istsr  16046  islindf  19014  decpmatval0  19432  pmatcollpw3lem  19451  ordtval  19857  dfac14  20285  fmval  20610  fmf  20612  blfvalps  21052  tmsval  21150  cfilfval  21869  caufval  21880  isibl  22338  elcpn  22503  iscgrg  24105  isuhgra  24500  uhgrac  24507  uhgraeq12d  24509  isuslgra  24545  isusgra  24546  usgraeq12d  24564  wlks  24721  wlkcompim  24728  wlkelwrd  24732  ex-dm  25362  isass  25516  isexid  25517  ismgmOLD  25520  locfinreflem  28078  pstmval  28109  cntnevol  28436  omsval  28501  sitgval  28538  elprob  28612  cndprobval  28636  rrvmbfm  28645  mrsubfval  29132  rdgprc0  29466  dfrdg2  29468  frrlem5e  29635  bdayval  29648  bdayfo  29675  nofulllem5  29706  brdomaing  29813  bpolylem  30038  bpolyval  30039  filnetlem4  30439  ismtyval  30536  aomclem6  31244  aomclem8  31246  dfac21  31251  uhg0e  32748  uhgres  32751  isfusgra  32796  fnxpdmdm  32828  offval0  33365  elbigo  33426  bnj1385  34292  bnj1400  34295  bnj1014  34419  bnj1015  34420  bnj1326  34483  bnj1321  34484  bnj1491  34514  dfrcl2  38193