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

Theorem nfrn 5789
 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 5531 . 2 ran 𝐴 = dom 𝐴
2 nfrn.1 . . . 4 𝑥𝐴
32nfcnv 5714 . . 3 𝑥𝐴
43nfdm 5788 . 2 𝑥dom 𝐴
51, 4nfcxfr 2953 1 𝑥ran 𝐴
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2936  ◡ccnv 5519  dom cdm 5520  ran crn 5521 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5032  df-opab 5094  df-cnv 5528  df-dm 5530  df-rn 5531 This theorem is referenced by:  nfima  5905  nff  6484  nffo  6565  fliftfun  7045  zfrep6  7641  ptbasfi  22196  utopsnneiplem  22863  restmetu  23187  itg2cnlem1  24375  acunirnmpt2  30433  acunirnmpt2f  30434  fnpreimac  30444  fsumiunle  30581  locfinreflem  31208  prodindf  31407  esumrnmpt2  31452  esumgect  31474  esum2d  31477  esumiun  31478  sigapildsys  31546  ldgenpisyslem1  31547  oms0  31680  breprexplema  32026  bnj1366  32226  exrecfnlem  34815  totbndbnd  35246  refsumcn  41702  suprnmpt  41841  disjrnmpt2  41858  disjf1o  41861  disjinfi  41863  choicefi  41872  rnmptbd2lem  41929  infnsuprnmpt  41931  rnmptbdlem  41936  rnmptss2  41938  rnmptssbi  41942  supxrleubrnmpt  42086  suprleubrnmpt  42102  infrnmptle  42103  infxrunb3rnmpt  42108  uzub  42111  supminfrnmpt  42125  infxrgelbrnmpt  42136  infrpgernmpt  42147  supminfxrrnmpt  42153  limsupubuz  42398  liminflelimsuplem  42460  stoweidlem27  42712  stoweidlem29  42714  stoweidlem31  42716  stoweidlem35  42720  stoweidlem59  42744  stoweidlem62  42747  stirlinglem5  42763  fourierdlem31  42823  fourierdlem53  42844  fourierdlem80  42871  fourierdlem93  42884  sge00  43058  sge0f1o  43064  sge0gerp  43077  sge0pnffigt  43078  sge0lefi  43080  sge0ltfirp  43082  sge0resplit  43088  sge0reuz  43129  iunhoiioolem  43357  smfpimcc  43482  smfsup  43488  smfsupxr  43490  smfinf  43492  smflimsup  43502  nfafv2  43817
 Copyright terms: Public domain W3C validator