Theorem dfdm4 5200

Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996.)

Assertion

Ref	Expression
dfdm4

Proof of Theorem dfdm4

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3112	. . . . 5
2		vex 3112	. . . . 5
3	1, 2	brcnv 5190	. . . 4
4	3	exbii 1667	. . 3
5	4	abbii 2591	. 2
6		dfrn2 5196	. 2
7		df-dm 5014	. 2
8	5, 6, 7	3eqtr4ri 2497	1

Syntax hints:  =wceq 1395  E.wex 1612  {cab 2442   class class class wbr 4452  `'ccnv 5003  domcdm 5004  rancrn 5005

This theorem is referenced by:  dmcnvcnv  5230  rncnvcnv  5231  rncoeq  5271  cnvimass  5362  cnvimarndm  5363  dminxp  5452  cnvsn0  5481  rnsnopg  5492  dmmpt  5507  dmco  5520  cores2  5525  cnvssrndm  5534  unidmrn  5542  dfdm2  5544  funimacnv  5665  foimacnv  5838  funcocnv2  5845  fimacnv  6019  f1opw2  6528  cnvexg  6746  tz7.48-3  7128  fopwdom  7645  sbthlem4  7650  fodomr  7688  f1opwfi  7844  zorn2lem4  8900  unbenlem  14426  gsumpropd2lem  15900  funsnfsupOLD  18256  pjdm  18738  paste  19795  hmeores  20272  icchmeo  21441  fcnvgreu  27514  ffsrn  27552  gsummpt2co  27771  coinfliprv  28421  itg2addnclem2  30067  lnmlmic  31034  conrel1d  37761  trclubg  37785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-cnv 5012  df-dm 5014  df-rn 5015