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

Theorem nfrn 5289
Description: Bound-variable hypothesis builder for range. (Contributed by NM, 1-Sep-1999.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypothesis
Ref Expression
nfrn.1 𝑥𝐴
Assertion
Ref Expression
nfrn 𝑥ran 𝐴

Proof of Theorem nfrn
StepHypRef Expression
1 df-rn 5049 . 2 ran 𝐴 = dom 𝐴
2 nfrn.1 . . . 4 𝑥𝐴
32nfcnv 5223 . . 3 𝑥𝐴
43nfdm 5288 . 2 𝑥dom 𝐴
51, 4nfcxfr 2749 1 𝑥ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2738  ccnv 5037  dom cdm 5038  ran crn 5039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049
This theorem is referenced by:  nfima  5393  nff  5954  nffo  6027  fliftfun  6462  zfrep6  7027  ptbasfi  21194  utopsnneiplem  21861  restmetu  22185  itg2cnlem1  23334  acunirnmpt2  28842  acunirnmpt2f  28843  locfinreflem  29235  esumrnmpt2  29457  esumgect  29479  esum2d  29482  esumiun  29483  sigapildsys  29552  ldgenpisyslem1  29553  oms0  29686  bnj1366  30154  totbndbnd  32758  refsumcn  38212  suprnmpt  38350  wessf1ornlem  38366  disjrnmpt2  38370  disjf1o  38373  disjinfi  38375  choicefi  38387  stoweidlem27  38920  stoweidlem29  38922  stoweidlem31  38924  stoweidlem35  38928  stoweidlem59  38952  stoweidlem62  38955  stirlinglem5  38971  fourierdlem31  39031  fourierdlem53  39052  fourierdlem80  39079  fourierdlem93  39092  sge00  39269  sge0f1o  39275  sge0gerp  39288  sge0pnffigt  39289  sge0lefi  39291  sge0ltfirp  39293  sge0resplit  39299  sge0reuz  39340  iunhoiioolem  39566
  Copyright terms: Public domain W3C validator