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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Ⅎwnfc 2908  {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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-opab 5168  df-mpt 5187

This theorem is used by:  ovmpt3rab1  7677  nfof  7697  mpocurryvald  8280  nfrdg  8415  mapxpen  9155  nfoi  9501  seqof2  14196  nfsum1  15850  nfsum  15851  fsumrlim  15971  fsumo1  15972  nfcprod1  16070  nfcprod  16071  gsum2d2  20181  prdsgsum  20188  dprd2d2  20253  gsumdixp  20541  pwsgprod  20552  mpfrcl  22387  ptbasfi  23893  ptcnplem  23933  ptcnp  23934  cnmptk2  23998  cnmpt2k  24000  xkocnv  24126  fsumcn  25184  itg2cnlem1  26075  nfitg  26088  itgfsum  26140  dvmptfsum  26288  itgulm2  26729  lgamgulm2  27356  nosupbnd2  28066  noinfbnd2  28081  fmptcof2  33244  fpwrelmap  33318  nfesum2  34666  sigapildsys  34788  oms0  34922  bnj1366  35452  exrecfnlem  38282  poimirlem26  38544  cdleme32d  41481  cdleme32f  41483  cdlemksv2  41884  cdlemkuv2  41904  hlhilset  42971  aomclem8  44047  binomcxplemdvsum  45324  refsum2cn  46024  fmuldfeq  46564  fprodcnlem  46580  fprodcn  46581  fnlimfv  46642  fnlimcnv  46646  fnlimfvre  46653  fnlimfvre2  46656  fnlimf  46657  fnlimabslt  46658  fprodcncf  46879  dvnmptdivc  46917  dvmptfprod  46924  dvnprodlem1  46925  stoweidlem26  47005  stoweidlem31  47010  stoweidlem34  47013  stoweidlem35  47014  stoweidlem42  47021  stoweidlem48  47027  stoweidlem59  47038  fourierdlem31  47117  fourierdlem112  47197  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0iunmpt  47397  hoicvrrex  47535  ovncvrrp  47543  ovnhoilem1  47580  ovnlecvr2  47589  vonicc  47664  smflim  47756  smfmullem4  47773  smflim2  47785  smflimmpt  47789  smfsup  47793  smfsupmpt  47794  smfinf  47797  smfinfmpt  47798  smflimsuplem2  47800  smflimsuplem5  47803  smflimsup  47807  smflimsupmpt  47808  smfliminf  47810  smfliminfmpt  47811  fsupdm  47821  finfdm  47825  aacllem  50908