Theorem nfmpt 5193

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Ⅎwnfc 2880  {copab 5157   ↦ cmpt 5176

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-opab 5158  df-mpt 5177

This theorem is referenced by:  ovmpt3rab1  7613  nfof  7625  mpocurryvald  8209  nfrdg  8342  mapxpen  9067  nfoi  9411  seqof2  13974  nfsum1  15604  nfsum  15605  fsumrlim  15725  fsumo1  15726  nfcprod1  15822  nfcprod  15823  gsum2d2  19894  prdsgsum  19901  dprd2d2  19966  gsumdixp  20245  pwsgprod  20256  mpfrcl  22031  ptbasfi  23516  ptcnplem  23556  ptcnp  23557  cnmptk2  23621  cnmpt2k  23623  xkocnv  23749  fsumcn  24808  itg2cnlem1  25709  nfitg  25723  itgfsum  25775  dvmptfsum  25926  itgulm2  26365  lgamgulm2  26993  nosupbnd2  27675  noinfbnd2  27690  fmptcof2  32661  fpwrelmap  32740  nfesum2  34126  sigapildsys  34247  oms0  34382  bnj1366  34913  exrecfnlem  37496  poimirlem26  37759  cdleme32d  40616  cdleme32f  40618  cdlemksv2  41019  cdlemkuv2  41039  hlhilset  42106  aomclem8  43218  binomcxplemdvsum  44512  refsum2cn  45199  fmuldfeq  45745  fprodcnlem  45761  fprodcn  45762  fnlimfv  45823  fnlimcnv  45827  fnlimfvre  45834  fnlimfvre2  45837  fnlimf  45838  fnlimabslt  45839  fprodcncf  46060  dvnmptdivc  46098  dvmptfprod  46105  dvnprodlem1  46106  stoweidlem26  46186  stoweidlem31  46191  stoweidlem34  46194  stoweidlem35  46195  stoweidlem42  46202  stoweidlem48  46208  stoweidlem59  46219  fourierdlem31  46298  fourierdlem112  46378  sge0iunmptlemfi  46573  sge0iunmptlemre  46575  sge0iunmpt  46578  hoicvrrex  46716  ovncvrrp  46724  ovnhoilem1  46761  ovnlecvr2  46770  vonicc  46845  smflim  46937  smfmullem4  46954  smflim2  46966  smflimmpt  46970  smfsup  46974  smfsupmpt  46975  smfinf  46978  smfinfmpt  46979  smflimsuplem2  46981  smflimsuplem5  46984  smflimsup  46988  smflimsupmpt  46989  smfliminf  46991  smfliminfmpt  46992  fsupdm  47002  finfdm  47006  aacllem  49962