Theorem dfdm4 5850

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 3433	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3433	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5837	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1850	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2803	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5843	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5641	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2770	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1542  ∃wex 1781  {cab 2714   class class class wbr 5085  ^◡ccnv 5630  dom cdm 5631  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  dmcnvcnv  5888  rncnvcnv  5889  rncoeq  5937  cnvimass  6047  cnvimarndm  6048  dminxp  6144  cnvsn0  6174  rnsnopg  6185  dmmpt  6204  dmco  6219  cores2  6224  cnvssrndm  6235  unidmrn  6243  dfdm2  6245  funimacnv  6579  foimacnv  6797  funcocnv2  6805  f1opw2  7622  cnvexg  7875  tz7.48-3  8383  fopwdom  9023  sbthlem4  9028  fodomr  9066  cnvfi  9110  fodomfir  9238  f1opwfi  9266  zorn2lem4  10421  trclublem  14957  relexpcnv  14997  unbenlem  16879  gsumpropd2lem  18647  pjdm  21687  paste  23259  hmeores  23736  icchmeo  24908  fcnvgreu  32745  ffsrn  32801  gsummpt2co  33109  tocycfvres1  33171  tocycfvres2  33172  cycpmfvlem  33173  cycpmfv3  33176  coinfliprv  34627  itg2addnclem2  37993  rncnv  38627  lnmlmic  43516  dmnonrel  44017  cnvrcl0  44052  conrel1d  44090