Theorem nfmpt 5200

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 5184	. 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 5171	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

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

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 5165  df-mpt 5184

This theorem is referenced by:  ovmpt3rab1  7627  nfof  7639  mpocurryvald  8226  nfrdg  8359  mapxpen  9084  nfoi  9443  seqof2  14001  nfsum1  15632  nfsum  15633  fsumrlim  15753  fsumo1  15754  nfcprod1  15850  nfcprod  15851  gsum2d2  19880  prdsgsum  19887  dprd2d2  19952  gsumdixp  20204  mpfrcl  21968  ptbasfi  23444  ptcnplem  23484  ptcnp  23485  cnmptk2  23549  cnmpt2k  23551  xkocnv  23677  fsumcn  24737  itg2cnlem1  25638  nfitg  25652  itgfsum  25704  dvmptfsum  25855  itgulm2  26294  lgamgulm2  26922  nosupbnd2  27604  noinfbnd2  27619  fmptcof2  32554  fpwrelmap  32629  nfesum2  34004  sigapildsys  34125  oms0  34261  bnj1366  34792  exrecfnlem  37340  poimirlem26  37613  cdleme32d  40411  cdleme32f  40413  cdlemksv2  40814  cdlemkuv2  40834  hlhilset  41901  pwsgprod  42505  aomclem8  43023  binomcxplemdvsum  44317  refsum2cn  45005  fmuldfeq  45554  fprodcnlem  45570  fprodcn  45571  fnlimfv  45634  fnlimcnv  45638  fnlimfvre  45645  fnlimfvre2  45648  fnlimf  45649  fnlimabslt  45650  fprodcncf  45871  dvnmptdivc  45909  dvmptfprod  45916  dvnprodlem1  45917  stoweidlem26  45997  stoweidlem31  46002  stoweidlem34  46005  stoweidlem35  46006  stoweidlem42  46013  stoweidlem48  46019  stoweidlem59  46030  fourierdlem31  46109  fourierdlem112  46189  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0iunmpt  46389  hoicvrrex  46527  ovncvrrp  46535  ovnhoilem1  46572  ovnlecvr2  46581  vonicc  46656  smflim  46748  smfmullem4  46765  smflim2  46777  smflimmpt  46781  smfsup  46785  smfsupmpt  46786  smfinf  46789  smfinfmpt  46790  smflimsuplem2  46792  smflimsuplem5  46795  smflimsup  46799  smflimsupmpt  46800  smfliminf  46802  smfliminfmpt  46803  fsupdm  46813  finfdm  46817  aacllem  49763