Theorem nfmpt 5185

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 5162	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2895	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2925	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1905	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5147	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2906	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2109  Ⅎwnfc 2888  {copab 5140   ↦ cmpt 5161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-opab 5141  df-mpt 5162

This theorem is referenced by:  ovmpt3rab1  7518  nfof  7530  mpocurryvald  8070  nfrdg  8229  mapxpen  8895  nfoi  9234  seqof2  13762  nfsum1  15382  nfsum  15383  nfsumOLD  15384  fsumrlim  15504  fsumo1  15505  nfcprod1  15601  nfcprod  15602  gsum2d2  19556  prdsgsum  19563  dprd2d2  19628  gsumdixp  19829  mpfrcl  21276  ptbasfi  22713  ptcnplem  22753  ptcnp  22754  cnmptk2  22818  cnmpt2k  22820  xkocnv  22946  fsumcn  24014  itg2cnlem1  24907  nfitg  24920  itgfsum  24972  dvmptfsum  25120  itgulm2  25549  lgamgulm2  26166  fmptcof2  30973  fpwrelmap  31047  nfesum2  31988  sigapildsys  32109  oms0  32243  bnj1366  32788  nosupbnd2  33898  noinfbnd2  33913  exrecfnlem  35529  poimirlem26  35782  cdleme32d  38437  cdleme32f  38439  cdlemksv2  38840  cdlemkuv2  38860  hlhilset  39927  pwsgprod  40249  aomclem8  40866  binomcxplemdvsum  41926  refsum2cn  42534  fmuldfeq  43078  fprodcnlem  43094  fprodcn  43095  fnlimfv  43158  fnlimcnv  43162  fnlimfvre  43169  fnlimfvre2  43172  fnlimf  43173  fnlimabslt  43174  fprodcncf  43395  dvnmptdivc  43433  dvmptfprod  43440  dvnprodlem1  43441  stoweidlem26  43521  stoweidlem31  43526  stoweidlem34  43529  stoweidlem35  43530  stoweidlem42  43537  stoweidlem48  43543  stoweidlem59  43554  fourierdlem31  43633  fourierdlem112  43713  sge0iunmptlemfi  43905  sge0iunmptlemre  43907  sge0iunmpt  43910  hoicvrrex  44048  ovncvrrp  44056  ovnhoilem1  44093  ovnlecvr2  44102  vonicc  44177  smflim  44263  smfmullem4  44279  smflim2  44290  smflimmpt  44294  smfsup  44298  smfsupmpt  44299  smfinf  44302  smfinfmpt  44303  smflimsuplem2  44305  smflimsuplem5  44308  smflimsup  44312  smflimsupmpt  44313  smfliminf  44315  smfliminfmpt  44316  aacllem  46457