Theorem nfmpt 5203

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 5187	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐵) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfmpt.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
3	2	nfcri 2914	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
4		nfmpt.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
5	4	nfeq2 2939	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐵
6	3, 5	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)
7	6	nfopab 5174	. 2 ⊢ Ⅎ𝑥{⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
8	1, 7	nfcxfr 2920	1 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ↦ 𝐵)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Ⅎwnfc 2907  {copab 5167   ↦ cmpt 5186

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-opab 5168  df-mpt 5187

This theorem is used by:  ovmpt3rab1  7672  nfof  7684  mpocurryvald  8268  nfrdg  8403  mapxpen  9141  nfoi  9486  seqof2  14124  nfsum1  15777  nfsum  15778  fsumrlim  15898  fsumo1  15899  nfcprod1  15997  nfcprod  15998  gsum2d2  20101  prdsgsum  20108  dprd2d2  20173  gsumdixp  20459  pwsgprod  20470  mpfrcl  22301  ptbasfi  23807  ptcnplem  23847  ptcnp  23848  cnmptk2  23912  cnmpt2k  23914  xkocnv  24040  fsumcn  25098  itg2cnlem1  25989  nfitg  26002  itgfsum  26054  dvmptfsum  26202  itgulm2  26645  lgamgulm2  27272  nosupbnd2  27952  noinfbnd2  27967  fmptcof2  33130  fpwrelmap  33204  nfesum2  34551  sigapildsys  34673  oms0  34808  bnj1366  35338  exrecfnlem  38133  poimirlem26  38395  cdleme32d  41317  cdleme32f  41319  cdlemksv2  41720  cdlemkuv2  41740  hlhilset  42807  aomclem8  43902  binomcxplemdvsum  45179  refsum2cn  45872  fmuldfeq  46413  fprodcnlem  46429  fprodcn  46430  fnlimfv  46491  fnlimcnv  46495  fnlimfvre  46502  fnlimfvre2  46505  fnlimf  46506  fnlimabslt  46507  fprodcncf  46728  dvnmptdivc  46766  dvmptfprod  46773  dvnprodlem1  46774  stoweidlem26  46854  stoweidlem31  46859  stoweidlem34  46862  stoweidlem35  46863  stoweidlem42  46870  stoweidlem48  46876  stoweidlem59  46887  fourierdlem31  46966  fourierdlem112  47046  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0iunmpt  47246  hoicvrrex  47384  ovncvrrp  47392  ovnhoilem1  47429  ovnlecvr2  47438  vonicc  47513  smflim  47605  smfmullem4  47622  smflim2  47634  smflimmpt  47638  smfsup  47642  smfsupmpt  47643  smfinf  47646  smfinfmpt  47647  smflimsuplem2  47649  smflimsuplem5  47652  smflimsup  47656  smflimsupmpt  47657  smfliminf  47659  smfliminfmpt  47660  fsupdm  47670  finfdm  47674  aacllem  50772