Theorem nfmpt 5163

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Ⅎwnfc 2961  {copab 5128   ↦ cmpt 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-opab 5129  df-mpt 5147

This theorem is referenced by:  ovmpt3rab1  7403  nfof  7414  mpocurryvald  7936  nfrdg  8050  mapxpen  8683  nfoi  8978  seqof2  13429  nfsum1  15046  nfsumw  15047  nfsum  15048  fsumrlim  15166  fsumo1  15167  nfcprod1  15264  nfcprod  15265  gsum2d2  19094  prdsgsum  19101  dprd2d2  19166  gsumdixp  19359  mpfrcl  20298  ptbasfi  22189  ptcnplem  22229  ptcnp  22230  cnmptk2  22294  cnmpt2k  22296  xkocnv  22422  fsumcn  23478  itg2cnlem1  24362  nfitg  24375  itgfsum  24427  dvmptfsum  24572  itgulm2  24997  lgamgulm2  25613  fmptcof2  30402  fpwrelmap  30469  nfesum2  31300  sigapildsys  31421  oms0  31555  bnj1366  32101  nosupbnd2  33216  exrecfnlem  34663  poimirlem26  34933  cdleme32d  37595  cdleme32f  37597  cdlemksv2  37998  cdlemkuv2  38018  hlhilset  39085  aomclem8  39681  binomcxplemdvsum  40707  refsum2cn  41315  fmuldfeq  41884  fprodcnlem  41900  fprodcn  41901  fnlimfv  41964  fnlimcnv  41968  fnlimfvre  41975  fnlimfvre2  41978  fnlimf  41979  fnlimabslt  41980  fprodcncf  42204  dvnmptdivc  42243  dvmptfprod  42250  dvnprodlem1  42251  stoweidlem26  42331  stoweidlem31  42336  stoweidlem34  42339  stoweidlem35  42340  stoweidlem42  42347  stoweidlem48  42353  stoweidlem59  42364  fourierdlem31  42443  fourierdlem112  42523  sge0iunmptlemfi  42715  sge0iunmptlemre  42717  sge0iunmpt  42720  hoicvrrex  42858  ovncvrrp  42866  ovnhoilem1  42903  ovnlecvr2  42912  vonicc  42987  smflim  43073  smfmullem4  43089  smflim2  43100  smflimmpt  43104  smfsup  43108  smfsupmpt  43109  smfinf  43112  smfinfmpt  43113  smflimsuplem2  43115  smflimsuplem5  43118  smflimsup  43122  smflimsupmpt  43123  smfliminf  43125  smfliminfmpt  43126  aacllem  44922