Theorem dfdm4 5877

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 3455	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3455	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5860	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1881	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2828	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5870	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5661	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2795	1 ⊢ dom 𝐴 = ran ◡𝐴

This proof depends on syntax axioms:   = wceq 1570  ∃wex 1812  {cab 2739   class class class wbr 5103  ^◡ccnv 5650  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  dmcnvcnv  5915  rncnvcnv  5916  rncoeq  5963  cnvimassrndm  6079  cnvimarndmOLD  6081  dminxp  6172  cnvimass  6198  cnvsn0  6211  rnsnopg  6222  dmmpt  6241  dmco  6256  cores2  6261  cnvssrndm  6273  unidmrn  6282  dfdm2  6284  funimacnv  6621  foimacnv  6842  funcocnv2  6850  f1opw2  7676  cnvexg  7936  tz7.48-3  8454  fopwdom  9104  sbthlem4  9109  fodomr  9147  cnvfi  9191  fodomfir  9319  f1opwfi  9345  zorn2lem4  10577  trclublem  15148  relexpcnv  15188  unbenlem  17086  gsumpropd2lem  18868  pjdm  22013  paste  23612  hmeores  24090  icchmeo  25262  fcnvgreu  33266  ffsrn  33320  gsummpt2co  33609  tocycfvres1  33671  tocycfvres2  33672  cycpmfvlem  33673  cycpmfv3  33676  coinfliprv  35115  itg2addnclem2  38590  rncnv  39238  lnmlmic  44089  dmnonrel  44589  cnvrcl0  44624  conrel1d  44662  cocanss1  45923