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

Theorem nfrn 5912
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 5649 . 2 ran 𝐴 = dom 𝐴
2 nfrn.1 . . . 4 𝑥𝐴
32nfcnv 5839 . . 3 𝑥𝐴
43nfdm 5911 . 2 𝑥dom 𝐴
51, 4nfcxfr 2906 1 𝑥ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2888  ccnv 5637  dom cdm 5638  ran crn 5639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-cnv 5646  df-dm 5648  df-rn 5649
This theorem is referenced by:  nfima  6026  nff  6669  nffo  6760  fliftfun  7262  zfrep6  7892  ptbasfi  22948  utopsnneiplem  23615  restmetu  23942  itg2cnlem1  25142  acunirnmpt2  31618  acunirnmpt2f  31619  fnpreimac  31629  fsumiunle  31767  nsgqusf1olem1  32231  nsgqusf1olem3  32233  locfinreflem  32461  prodindf  32662  esumrnmpt2  32707  esumgect  32729  esum2d  32732  esumiun  32733  sigapildsys  32801  ldgenpisyslem1  32802  oms0  32937  breprexplema  33283  bnj1366  33481  exrecfnlem  35879  totbndbnd  36277  refsumcn  43309  disjrnmpt2  43481  disjf1o  43484  disjinfi  43486  choicefi  43495  rnmptbd2lem  43550  infnsuprnmpt  43552  rnmptbdlem  43557  rnmptss2  43559  rnmptssbi  43563  supxrleubrnmpt  43715  suprleubrnmpt  43731  infrnmptle  43732  infxrunb3rnmpt  43737  uzub  43740  supminfrnmpt  43754  infxrgelbrnmpt  43763  infrpgernmpt  43774  supminfxrrnmpt  43780  limsupubuz  44028  liminflelimsuplem  44090  stoweidlem27  44342  stoweidlem29  44344  stoweidlem31  44346  stoweidlem35  44350  stoweidlem59  44374  stoweidlem62  44377  stirlinglem5  44393  fourierdlem31  44453  fourierdlem80  44501  fourierdlem93  44514  sge00  44691  sge0f1o  44697  sge0gerp  44710  sge0pnffigt  44711  sge0lefi  44713  sge0ltfirp  44715  sge0resplit  44721  sge0reuz  44762  iunhoiioolem  44990  smfpimcc  45123  smfsup  45129  smfsupxr  45131  smfinf  45133  smflimsup  45143  nfafv2  45524
  Copyright terms: Public domain W3C validator