Theorem dfdm4 5844

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

Syntax hints:   = wceq 1541  ∃wex 1780  {cab 2714   class class class wbr 5098  ^◡ccnv 5623  dom cdm 5624  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  dmcnvcnv  5882  rncnvcnv  5883  rncoeq  5931  cnvimass  6041  cnvimarndm  6042  dminxp  6138  cnvsn0  6168  rnsnopg  6179  dmmpt  6198  dmco  6213  cores2  6218  cnvssrndm  6229  unidmrn  6237  dfdm2  6239  funimacnv  6573  foimacnv  6791  funcocnv2  6799  f1opw2  7613  cnvexg  7866  tz7.48-3  8375  fopwdom  9013  sbthlem4  9018  fodomr  9056  cnvfi  9100  fodomfir  9228  f1opwfi  9256  zorn2lem4  10409  trclublem  14918  relexpcnv  14958  unbenlem  16836  gsumpropd2lem  18604  pjdm  21662  paste  23238  hmeores  23715  icchmeo  24894  icchmeoOLD  24895  fcnvgreu  32751  ffsrn  32807  gsummpt2co  33131  tocycfvres1  33192  tocycfvres2  33193  cycpmfvlem  33194  cycpmfv3  33197  coinfliprv  34640  itg2addnclem2  37873  rncnv  38499  lnmlmic  43330  dmnonrel  43831  cnvrcl0  43866  conrel1d  43904