Theorem nfrn 5905

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

Step	Hyp	Ref	Expression
1		df-rn 5642	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5832	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5904	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2889	1 ⊢ Ⅎ𝑥ran 𝐴

Syntax hints:  Ⅎwnfc 2876  ^◡ccnv 5630  dom cdm 5631  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  nfima  6028  nff  6666  nffo  6753  fliftfun  7269  zfrep6  7913  ptbasfi  23444  utopsnneiplem  24111  restmetu  24434  itg2cnlem1  25638  acunirnmpt2  32557  acunirnmpt2f  32558  fnpreimac  32568  fsumiunle  32727  prodindf  32759  nsgqusf1olem1  33357  nsgqusf1olem3  33359  locfinreflem  33803  esumrnmpt2  34031  esumgect  34053  esum2d  34056  esumiun  34057  sigapildsys  34125  ldgenpisyslem1  34126  oms0  34261  breprexplema  34594  bnj1366  34792  exrecfnlem  37340  totbndbnd  37756  modelaxreplem3  44943  refsumcn  44997  disjrnmpt2  45155  disjf1o  45158  disjinfi  45159  choicefi  45167  rnmptbd2lem  45215  infnsuprnmpt  45217  rnmptbdlem  45222  rnmptss2  45224  rnmptssbi  45227  supxrleubrnmpt  45375  suprleubrnmpt  45391  infrnmptle  45392  infxrunb3rnmpt  45397  uzub  45400  supminfrnmpt  45414  infxrgelbrnmpt  45423  infrpgernmpt  45434  supminfxrrnmpt  45440  limsupubuz  45684  liminflelimsuplem  45746  stoweidlem27  45998  stoweidlem29  46000  stoweidlem31  46002  stoweidlem35  46006  stoweidlem59  46030  stoweidlem62  46033  stirlinglem5  46049  fourierdlem31  46109  fourierdlem80  46157  fourierdlem93  46170  sge00  46347  sge0f1o  46353  sge0gerp  46366  sge0pnffigt  46367  sge0lefi  46369  sge0ltfirp  46371  sge0resplit  46377  sge0reuz  46418  iunhoiioolem  46646  smfpimcc  46779  smfsup  46785  smfsupxr  46787  smfinf  46789  smflimsup  46799  nfafv2  47192