Theorem dfdm4 5838

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

Assertion

Ref	Expression
dfdm4	⊢ dom 𝐴 = ran ◡𝐴

Proof of Theorem dfdm4

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

Step	Hyp	Ref	Expression
1		vex 3440	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3440	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5825	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1848	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2796	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5831	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5629	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2763	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1540  ∃wex 1779  {cab 2707   class class class wbr 5092  ^◡ccnv 5618  dom cdm 5619  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  dmcnvcnv  5875  rncnvcnv  5876  rncoeq  5923  cnvimass  6033  cnvimarndm  6034  dminxp  6129  cnvsn0  6159  rnsnopg  6170  dmmpt  6189  dmco  6203  cores2  6208  cnvssrndm  6219  unidmrn  6227  dfdm2  6229  funimacnv  6563  foimacnv  6781  funcocnv2  6789  f1opw2  7604  cnvexg  7857  tz7.48-3  8366  fopwdom  9002  sbthlem4  9007  fodomr  9045  cnvfi  9090  fodomfir  9218  f1opwfi  9246  zorn2lem4  10393  trclublem  14902  relexpcnv  14942  unbenlem  16820  gsumpropd2lem  18553  pjdm  21614  paste  23179  hmeores  23656  icchmeo  24836  icchmeoOLD  24837  fcnvgreu  32616  ffsrn  32672  gsummpt2co  33001  tocycfvres1  33052  tocycfvres2  33053  cycpmfvlem  33054  cycpmfv3  33057  coinfliprv  34451  itg2addnclem2  37652  rncnv  38274  lnmlmic  43061  dmnonrel  43563  cnvrcl0  43598  conrel1d  43636