Theorem nfmpt 5205

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.)

Hypotheses

Ref	Expression
nfmpt.1	⊢ Ⅎ𝑥𝐴
nfmpt.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfmpt	⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem nfmpt

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt 5189	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2883	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2909	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1899	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5176	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2876  {copab 5169   ↦ cmpt 5188

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-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-opab 5170  df-mpt 5189

This theorem is referenced by:  ovmpt3rab1  7647  nfof  7659  mpocurryvald  8249  nfrdg  8382  mapxpen  9107  nfoi  9467  seqof2  14025  nfsum1  15656  nfsum  15657  fsumrlim  15777  fsumo1  15778  nfcprod1  15874  nfcprod  15875  gsum2d2  19904  prdsgsum  19911  dprd2d2  19976  gsumdixp  20228  mpfrcl  21992  ptbasfi  23468  ptcnplem  23508  ptcnp  23509  cnmptk2  23573  cnmpt2k  23575  xkocnv  23701  fsumcn  24761  itg2cnlem1  25662  nfitg  25676  itgfsum  25728  dvmptfsum  25879  itgulm2  26318  lgamgulm2  26946  nosupbnd2  27628  noinfbnd2  27643  fmptcof2  32581  fpwrelmap  32656  nfesum2  34031  sigapildsys  34152  oms0  34288  bnj1366  34819  exrecfnlem  37367  poimirlem26  37640  cdleme32d  40438  cdleme32f  40440  cdlemksv2  40841  cdlemkuv2  40861  hlhilset  41928  pwsgprod  42532  aomclem8  43050  binomcxplemdvsum  44344  refsum2cn  45032  fmuldfeq  45581  fprodcnlem  45597  fprodcn  45598  fnlimfv  45661  fnlimcnv  45665  fnlimfvre  45672  fnlimfvre2  45675  fnlimf  45676  fnlimabslt  45677  fprodcncf  45898  dvnmptdivc  45936  dvmptfprod  45943  dvnprodlem1  45944  stoweidlem26  46024  stoweidlem31  46029  stoweidlem34  46032  stoweidlem35  46033  stoweidlem42  46040  stoweidlem48  46046  stoweidlem59  46057  fourierdlem31  46136  fourierdlem112  46216  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  hoicvrrex  46554  ovncvrrp  46562  ovnhoilem1  46599  ovnlecvr2  46608  vonicc  46683  smflim  46775  smfmullem4  46792  smflim2  46804  smflimmpt  46808  smfsup  46812  smfsupmpt  46813  smfinf  46816  smfinfmpt  46817  smflimsuplem2  46819  smflimsuplem5  46822  smflimsup  46826  smflimsupmpt  46827  smfliminf  46829  smfliminfmpt  46830  fsupdm  46840  finfdm  46844  aacllem  49790