Theorem dfdm4 5849

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 3448	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3448	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5836	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1848	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2796	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5842	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5641	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2763	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1540  ∃wex 1779  {cab 2707   class class class wbr 5102  ^◡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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  dmcnvcnv  5886  rncnvcnv  5887  rncoeq  5932  cnvimass  6042  cnvimarndm  6043  dminxp  6141  cnvsn0  6171  rnsnopg  6182  dmmpt  6201  dmco  6215  cores2  6220  cnvssrndm  6232  unidmrn  6240  dfdm2  6242  funimacnv  6581  foimacnv  6799  funcocnv2  6807  f1opw2  7624  cnvexg  7880  tz7.48-3  8389  fopwdom  9026  sbthlem4  9031  fodomr  9069  cnvfi  9117  fodomfir  9255  f1opwfi  9283  zorn2lem4  10428  trclublem  14937  relexpcnv  14977  unbenlem  16855  gsumpropd2lem  18582  pjdm  21592  paste  23157  hmeores  23634  icchmeo  24814  icchmeoOLD  24815  fcnvgreu  32570  ffsrn  32625  gsummpt2co  32961  tocycfvres1  33040  tocycfvres2  33041  cycpmfvlem  33042  cycpmfv3  33045  coinfliprv  34447  itg2addnclem2  37639  rncnv  38261  lnmlmic  43050  dmnonrel  43552  cnvrcl0  43587  conrel1d  43625