Theorem nfrn 5944

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 5674	. 2 ⊢ ran 𝐴 = dom ◡𝐴
2		nfrn.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	nfcnv 5866	. . 3 ⊢ Ⅎ𝑥◡𝐴
4	3	nfdm 5943	. 2 ⊢ Ⅎ𝑥dom ◡𝐴
5	1, 4	nfcxfr 2925	1 ⊢ Ⅎ𝑥ran 𝐴

This proof depends on syntax axioms:  Ⅎwnfc 2912  ^◡ccnv 5662  dom cdm 5663  ran crn 5664

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  nfima  6072  nff  6705  nffo  6795  fliftfun  7319  zfrep6OLD  7958  ptbasfi  23789  utopsnneiplem  24455  restmetu  24778  itg2cnlem1  25971  acunirnmpt2  33076  acunirnmpt2f  33077  fnpreimac  33086  fsumiunle  33243  prodindf  33252  nsgqusf1olem1  33786  nsgqusf1olem3  33788  locfinreflem  34294  esumrnmpt2  34522  esumgect  34544  esum2d  34547  esumiun  34548  sigapildsys  34617  ldgenpisyslem1  34618  oms0  34752  breprexplema  35082  bnj1366  35282  exrecfnlem  38082  totbndbnd  38498  modelaxreplem3  45747  refsumcn  45808  disjrnmpt2  45964  disjf1o  45967  disjinfi  45968  choicefi  45975  rnmptbd2lem  46021  infnsuprnmpt  46023  rnmptbdlem  46028  rnmptss2  46030  rnmptssbi  46033  supxrleubrnmpt  46178  suprleubrnmpt  46194  infrnmptle  46195  infxrunb3rnmpt  46200  uzub  46203  supminfrnmpt  46217  infxrgelbrnmpt  46226  infrpgernmpt  46237  supminfxrrnmpt  46243  limsupubuz  46485  liminflelimsuplem  46547  stoweidlem27  46799  stoweidlem29  46801  stoweidlem31  46803  stoweidlem35  46807  stoweidlem59  46831  stoweidlem62  46834  stirlinglem5  46850  fourierdlem31  46910  fourierdlem80  46958  fourierdlem93  46971  sge00  47148  sge0f1o  47154  sge0gerp  47167  sge0pnffigt  47168  sge0lefi  47170  sge0ltfirp  47172  sge0resplit  47178  sge0reuz  47219  iunhoiioolem  47447  smfpimcc  47580  smfsup  47586  smfsupxr  47588  smfinf  47590  smflimsup  47600  nfafv2  48013