Theorem nfrn 5368

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	|- F/_ x A

Assertion

Ref	Expression
nfrn	|- F/_ x ran A

Proof of Theorem nfrn

Step	Hyp	Ref	Expression
1		df-rn 5125	. 2 |- ran A = dom `' A
2		nfrn.1	. . . 4 |- F/_ x A
3	2	nfcnv 5301	. . 3 |- F/_ x `' A
4	3	nfdm 5367	. 2 |- F/_ x dom `' A
5	1, 4	nfcxfr 2762	1 |- F/_ x ran A

Syntax hints:   F/_wnfc 2751   `'ccnv 5113   dom cdm 5114   ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  nfima  5474  nff  6041  nffo  6114  fliftfun  6562  zfrep6  7134  ptbasfi  21384  utopsnneiplem  22051  restmetu  22375  itg2cnlem1  23528  acunirnmpt2  29460  acunirnmpt2f  29461  fsumiunle  29575  locfinreflem  29907  prodindf  30085  esumrnmpt2  30130  esumgect  30152  esum2d  30155  esumiun  30156  sigapildsys  30225  ldgenpisyslem1  30226  oms0  30359  breprexplema  30708  bnj1366  30900  totbndbnd  33588  refsumcn  39189  suprnmpt  39355  wessf1ornlem  39371  disjrnmpt2  39375  disjf1o  39378  disjinfi  39380  choicefi  39392  rnmptbd2lem  39463  infnsuprnmpt  39465  rnmptbdlem  39470  rnmptss2  39472  rnmptssbi  39477  supxrleubrnmpt  39632  suprleubrnmpt  39649  infrnmptle  39650  infxrunb3rnmpt  39655  uzub  39658  supminfrnmpt  39672  infxrgelbrnmpt  39683  infrpgernmpt  39695  supminfxrrnmpt  39701  limsupubuz  39945  liminflelimsuplem  40007  stoweidlem27  40244  stoweidlem29  40246  stoweidlem31  40248  stoweidlem35  40252  stoweidlem59  40276  stoweidlem62  40279  stirlinglem5  40295  fourierdlem31  40355  fourierdlem53  40376  fourierdlem80  40403  fourierdlem93  40416  sge00  40593  sge0f1o  40599  sge0gerp  40612  sge0pnffigt  40613  sge0lefi  40615  sge0ltfirp  40617  sge0resplit  40623  sge0reuz  40664  iunhoiioolem  40889  smfpimcc  41014  smfsup  41020  smfsupxr  41022  smfinf  41024  smflimsup  41034