Theorem nfmpt1 5201

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.)

Assertion

Ref	Expression
nfmpt1	⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)

Proof of Theorem nfmpt1

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-mpt 5184	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfopab1 5172	. 2 ⊢ Ⅎ𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
3	1, 2	nfcxfr 2889	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2876  {copab 5164   ↦ cmpt 5183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-opab 5165  df-mpt 5184

This theorem is referenced by:  nffvmpt1  6851  fvmptss  6962  fvmptd3f  6965  mpteqb  6969  fvmptf  6971  ralrnmptw  7048  ralrnmpt  7050  f1ompt  7065  fompt  7072  f1mpt  7218  fliftfun  7269  rdgsucmptf  8373  rdgsucmptnf  8374  frsucmpt  8383  frsucmptn  8384  dom2lem  8940  mapxpen  9084  cnfcom3clem  9634  ttrclselem1  9654  ttrclselem2  9655  infxpenc2lem2  9949  dfac8clem  9961  acnlem  9977  fin23lem32  10273  axcc3  10367  ac6num  10408  nfcprod1  15850  yonedalem4b  18213  prdsgsum  19887  cayleyhamilton1  22755  neiptopreu  22996  2ndcdisj  23319  ptcnp  23485  cnmpt11  23526  cnmptk2  23549  xkocnv  23677  utopsnneiplem  24111  restmetu  24434  mbfposr  25529  mbfsup  25541  itg1climres  25591  itg2splitlem  25625  itg2split  25626  itg2cnlem1  25638  nfitg1  25651  dvlipcn  25875  lhop2  25896  dvfsumabs  25905  itgparts  25930  itgsubstlem  25931  itgulm2  26294  lgamgulm2  26922  lgseisenlem2  27263  istrkg2ld  28363  cnlnadjlem5  31973  acunirnmpt2  32557  acunirnmpt2f  32558  aciunf1lem  32559  ofpreima  32562  fnpreimac  32568  disjdsct  32599  fpwrelmap  32629  prodindf  32759  elrgspnsubrunlem2  33172  nsgqusf1olem1  33357  nsgqusf1olem3  33359  elrspunidl  33372  fedgmullem2  33599  locfinreflem  33803  nfesum1  34003  esumc  34014  esumrnmpt2  34031  esumsup  34052  esumgect  34053  esum2d  34056  sigapildsys  34125  ldgenpisyslem1  34126  voliune  34192  oms0  34261  rrvadd  34416  ballotlem7  34500  breprexplema  34594  cvmcov  35223  rdgssun  37339  exrecfnlem  37340  phpreu  37571  matunitlindflem2  37584  poimirlem16  37603  poimirlem19  37606  itg2addnclem  37638  ftc1anclem5  37664  totbndbnd  37756  pwsgprod  42505  mzpsubmpt  42704  eq0rabdioph  42737  eqrabdioph  42738  aomclem8  43023  binomcxplemdvbinom  44315  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  refsumcn  44997  refsum2cnlem1  45004  disjrnmpt2  45155  disjf1o  45158  disjinfi  45159  choicefi  45167  axccdom  45189  rnmptbd2lem  45215  infnsuprnmpt  45217  rnmptbdlem  45222  rnmptss2  45224  rnmptssbi  45227  supxrleubrnmpt  45375  suprleubrnmpt  45391  infrnmptle  45392  infxrunb3rnmpt  45397  uzub  45400  supminfrnmpt  45414  infxrgelbrnmpt  45423  infrpgernmpt  45434  supminfxrrnmpt  45440  fmuldfeqlem1  45553  fmuldfeq  45554  climneg  45581  climdivf  45583  mullimc  45587  idlimc  45597  sumnnodd  45601  neglimc  45618  addlimc  45619  0ellimcdiv  45620  fnlimfvre  45645  fnlimabslt  45650  climreclmpt  45655  climfveqmpt2  45664  climeldmeqmpt2  45666  climeqmpt  45668  limsupubuz  45684  climinfmpt  45686  limsupubuzmpt  45690  limsupequzmptlem  45699  limsupre2mpt  45701  limsupre3mpt  45705  limsupreuzmpt  45710  liminflelimsuplem  45746  liminfvalxr  45754  liminfvalxrmpt  45757  liminfltlem  45775  liminflbuz2  45786  liminfpnfuz  45787  xlimmnfmpt  45814  xlimpnfmpt  45815  xlimpnfxnegmnf2  45829  cncfmptssg  45842  cncfshift  45845  cncficcgt0  45859  cncfiooicclem1  45864  dvnmul  45914  dvmptfprod  45916  itgsin0pilem1  45921  ibliccsinexp  45922  itgsinexplem1  45925  itgsinexp  45926  iblspltprt  45944  itgsubsticclem  45946  stoweidlem16  45987  stoweidlem18  45989  stoweidlem19  45990  stoweidlem20  45991  stoweidlem22  45993  stoweidlem23  45994  stoweidlem27  45998  stoweidlem31  46002  stoweidlem32  46003  stoweidlem34  46005  stoweidlem35  46006  stoweidlem36  46007  stoweidlem40  46011  stoweidlem41  46012  stoweidlem42  46013  stoweidlem43  46014  stoweidlem44  46015  stoweidlem45  46016  stoweidlem48  46019  stoweidlem51  46022  stoweidlem55  46026  stoweidlem59  46030  stoweidlem60  46031  stoweidlem62  46033  wallispilem5  46040  stirlinglem4  46048  stirlinglem5  46049  stirlinglem8  46052  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  stirlinglem14  46058  stirlinglem15  46059  stirling  46060  fourierdlem16  46094  fourierdlem21  46099  fourierdlem22  46100  fourierdlem68  46145  fourierdlem73  46150  fourierdlem80  46157  fourierdlem89  46166  fourierdlem91  46168  fourierdlem93  46170  fourierdlem103  46180  fourierdlem104  46181  fourierdlem112  46189  fourierdlem115  46192  fourierd  46193  fourierclimd  46194  etransclem48  46253  sge00  46347  sge0revalmpt  46349  sge0f1o  46353  sge0fsummpt  46361  sge0gerp  46366  sge0pnffigt  46367  sge0lefi  46369  sge0ltfirp  46371  sge0resplit  46377  sge0iunmptlemfi  46384  sge0iunmpt  46389  sge0xadd  46406  sge0fsummptf  46407  sge0gtfsumgt  46414  sge0reuz  46418  iundjiun  46431  meaiuninc3v  46455  omeiunltfirp  46490  omeiunlempt  46491  hoicvrrex  46527  ovncvrrp  46535  ovnhoilem1  46572  ovnlecvr2  46581  opnvonmbllem1  46603  iunhoiioolem  46646  smfpimltmpt  46717  issmfdmpt  46719  smfconst  46720  smfpimltxrmptf  46729  smflimlem2  46743  smflim  46748  smfpimgtmpt  46752  smfpimgtxrmptf  46755  smfpimcclem  46778  smfpimcc  46779  smflimmpt  46781  smfsupmpt  46786  smfsupxr  46787  smfinfmpt  46790  smflimsuplem2  46792  smflimsuplem7  46797  smflimsupmpt  46800  smfliminfmpt  46803  cfsetsnfsetf  47032  1arymaptfo  48605  2arymaptfo  48616  setrec2mpt  49659  aacllem  49763