Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfdm4 Structured version   Visualization version   GIF version

Theorem dfdm4 5471
 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.
StepHypRef Expression
1 vex 3343 . . . . 5 𝑦 ∈ V
2 vex 3343 . . . . 5 𝑥 ∈ V
31, 2brcnv 5460 . . . 4 (𝑦𝐴𝑥𝑥𝐴𝑦)
43exbii 1923 . . 3 (∃𝑦 𝑦𝐴𝑥 ↔ ∃𝑦 𝑥𝐴𝑦)
54abbii 2877 . 2 {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥} = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
6 dfrn2 5466 . 2 ran 𝐴 = {𝑥 ∣ ∃𝑦 𝑦𝐴𝑥}
7 df-dm 5276 . 2 dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦}
85, 6, 73eqtr4ri 2793 1 dom 𝐴 = ran 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1632  ∃wex 1853  {cab 2746   class class class wbr 4804  ◡ccnv 5265  dom cdm 5266  ran crn 5267 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-cnv 5274  df-dm 5276  df-rn 5277 This theorem is referenced by:  dmcnvcnv  5503  rncnvcnv  5504  rncoeq  5544  cnvimass  5643  cnvimarndm  5644  dminxp  5732  cnvsn0  5761  rnsnopg  5773  dmmpt  5791  dmco  5804  cores2  5809  cnvssrndm  5818  unidmrn  5826  dfdm2  5828  funimacnv  6131  foimacnv  6315  funcocnv2  6322  fimacnv  6510  f1opw2  7053  cnvexg  7277  tz7.48-3  7708  fopwdom  8233  sbthlem4  8238  fodomr  8276  f1opwfi  8435  zorn2lem4  9513  trclublem  13935  relexpcnv  13974  unbenlem  15814  gsumpropd2lem  17474  pjdm  20253  paste  21300  hmeores  21776  icchmeo  22941  fcnvgreu  29781  ffsrn  29813  gsummpt2co  30089  coinfliprv  30853  itg2addnclem2  33775  rncnv  34394  lnmlmic  38160  dmnonrel  38398  cnvrcl0  38434  conrel1d  38457
 Copyright terms: Public domain W3C validator