Theorem dfdm4 5905

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 3483	. . . . 5 ⊢ 𝑦 ∈ V
2		vex 3483	. . . . 5 ⊢ 𝑥 ∈ V
3	1, 2	brcnv 5892	. . . 4 ⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦)
4	3	exbii 1847	. . 3 ⊢ (∃𝑦 𝑦◡𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
5	4	abbii 2808	. 2 ⊢ {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6		dfrn2 5898	. 2 ⊢ ran ◡𝐴 = {𝑥 ∣ ∃𝑦 𝑦◡𝐴𝑥}
7		df-dm 5694	. 2 ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
8	5, 6, 7	3eqtr4ri 2775	1 ⊢ dom 𝐴 = ran ◡𝐴

Syntax hints:   = wceq 1539  ∃wex 1778  {cab 2713   class class class wbr 5142  ^◡ccnv 5683  dom cdm 5684  ran crn 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695

This theorem is referenced by:  dmcnvcnv  5943  rncnvcnv  5944  rncoeq  5989  cnvimass  6099  cnvimarndm  6100  dminxp  6199  cnvsn0  6229  rnsnopg  6240  dmmpt  6259  dmco  6273  cores2  6278  cnvssrndm  6290  unidmrn  6298  dfdm2  6300  funimacnv  6646  foimacnv  6864  funcocnv2  6872  f1opw2  7689  cnvexg  7947  tz7.48-3  8485  fopwdom  9121  sbthlem4  9127  fodomr  9169  cnvfi  9217  fodomfir  9369  f1opwfi  9397  zorn2lem4  10540  trclublem  15035  relexpcnv  15075  unbenlem  16947  gsumpropd2lem  18693  pjdm  21728  paste  23303  hmeores  23780  icchmeo  24972  icchmeoOLD  24973  fcnvgreu  32684  ffsrn  32741  gsummpt2co  33052  tocycfvres1  33131  tocycfvres2  33132  cycpmfvlem  33133  cycpmfv3  33136  coinfliprv  34486  itg2addnclem2  37680  rncnv  38302  lnmlmic  43105  dmnonrel  43608  cnvrcl0  43643  conrel1d  43681