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

Theorem nfrn 5475
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 5229 . 2 ran 𝐴 = dom 𝐴
2 nfrn.1 . . . 4 𝑥𝐴
32nfcnv 5408 . . 3 𝑥𝐴
43nfdm 5474 . 2 𝑥dom 𝐴
51, 4nfcxfr 2864 1 𝑥ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wnfc 2853  ccnv 5217  dom cdm 5218  ran crn 5219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761  df-opab 4821  df-cnv 5226  df-dm 5228  df-rn 5229
This theorem is referenced by:  nfima  5584  nff  6154  nffo  6227  fliftfun  6677  zfrep6  7251  ptbasfi  21507  utopsnneiplem  22173  restmetu  22497  itg2cnlem1  23648  acunirnmpt2  29690  acunirnmpt2f  29691  fsumiunle  29805  locfinreflem  30137  prodindf  30315  esumrnmpt2  30360  esumgect  30382  esum2d  30385  esumiun  30386  sigapildsys  30455  ldgenpisyslem1  30456  oms0  30589  breprexplema  30938  bnj1366  31128  totbndbnd  33820  refsumcn  39605  suprnmpt  39771  wessf1ornlem  39787  disjrnmpt2  39791  disjf1o  39794  disjinfi  39796  choicefi  39808  rnmptbd2lem  39879  infnsuprnmpt  39881  rnmptbdlem  39886  rnmptss2  39888  rnmptssbi  39893  supxrleubrnmpt  40047  suprleubrnmpt  40064  infrnmptle  40065  infxrunb3rnmpt  40070  uzub  40073  supminfrnmpt  40087  infxrgelbrnmpt  40098  infrpgernmpt  40110  supminfxrrnmpt  40116  limsupubuz  40365  liminflelimsuplem  40427  stoweidlem27  40664  stoweidlem29  40666  stoweidlem31  40668  stoweidlem35  40672  stoweidlem59  40696  stoweidlem62  40699  stirlinglem5  40715  fourierdlem31  40775  fourierdlem53  40796  fourierdlem80  40823  fourierdlem93  40836  sge00  41013  sge0f1o  41019  sge0gerp  41032  sge0pnffigt  41033  sge0lefi  41035  sge0ltfirp  41037  sge0resplit  41043  sge0reuz  41084  iunhoiioolem  41312  smfpimcc  41437  smfsup  41443  smfsupxr  41445  smfinf  41447  smflimsup  41457
  Copyright terms: Public domain W3C validator