Theorem dfdm4 5920

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 3492	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3492	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5907	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1846	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2812	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5913	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5710	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2779	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1537  ∃wex 1777  {cab 2717   class class class wbr 5166  ^◡ccnv 5699  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  dmcnvcnv  5958  rncnvcnv  5959  rncoeq  6002  cnvimass  6111  cnvimarndm  6112  dminxp  6211  cnvsn0  6241  rnsnopg  6252  dmmpt  6271  dmco  6285  cores2  6290  cnvssrndm  6302  unidmrn  6310  dfdm2  6312  funimacnv  6659  foimacnv  6879  funcocnv2  6887  fimacnvOLD  7104  f1opw2  7705  cnvexg  7964  tz7.48-3  8500  fopwdom  9146  sbthlem4  9152  fodomr  9194  cnvfi  9243  fodomfir  9396  f1opwfi  9426  zorn2lem4  10568  trclublem  15044  relexpcnv  15084  unbenlem  16955  gsumpropd2lem  18717  pjdm  21750  paste  23323  hmeores  23800  icchmeo  24990  icchmeoOLD  24991  fcnvgreu  32691  ffsrn  32743  gsummpt2co  33031  tocycfvres1  33103  tocycfvres2  33104  cycpmfvlem  33105  cycpmfv3  33108  coinfliprv  34447  itg2addnclem2  37632  rncnv  38256  lnmlmic  43045  dmnonrel  43552  cnvrcl0  43587  conrel1d  43625