Theorem nfmpt1 5214

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 5197	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
2		nfopab1 5185	. 2 ⊢ Ⅎ𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
3	1, 2	nfcxfr 2929	1 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵)

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Ⅎwnfc 2916  {copab 5177   ↦ cmpt 5196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-opab 5178  df-mpt 5197

This theorem is referenced by:  nffvmpt1  6893  fvmptss  7003  fvmptd3f  7006  mpteqb  7010  fvmptf  7012  ralrnmptw  7090  ralrnmpt  7092  f1ompt  7107  fompt  7114  f1mpt  7260  fliftfun  7311  rdgsucmptf  8414  rdgsucmptnf  8415  frsucmpt  8424  frsucmptn  8425  dom2lem  8988  mapxpen  9130  cnfcom3clem  9673  ttrclselem1  9693  ttrclselem2  9694  infxpenc2lem2  10003  dfac8clem  10015  acnlem  10031  fin23lem32  10327  axcc3  10421  ac6num  10462  nfcprod1  15961  yonedalem4b  18331  prdsgsum  20050  pwsgprod  20410  cayleyhamilton1  23017  neiptopreu  23258  2ndcdisj  23581  ptcnp  23747  cnmpt11  23788  cnmptk2  23811  xkocnv  23939  utopsnneiplem  24372  restmetu  24695  mbfposr  25779  mbfsup  25791  itg1climres  25841  itg2splitlem  25875  itg2split  25876  itg2cnlem1  25888  nfitg1  25901  dvlipcn  26121  lhop2  26142  dvfsumabs  26150  itgparts  26174  itgsubstlem  26175  itgulm2  26537  lgamgulm2  27165  lgseisenlem2  27505  istrkg2ld  28694  cnlnadjlem5  32363  acunirnmpt2  32945  acunirnmpt2f  32946  aciunf1lem  32947  ofpreima  32950  fnpreimac  32955  disjdsct  32988  fpwrelmap  33018  prodindf  33122  suppgsumssiun  33332  elrgspnsubrunlem2  33508  nsgqusf1olem1  33665  nsgqusf1olem3  33667  elrspunidl  33679  deg1prod  33817  mplvrpmga  33879  esplyfval1  33907  fedgmullem2  33964  locfinreflem  34174  nfesum1  34374  esumc  34385  esumrnmpt2  34402  esumsup  34423  esumgect  34424  esum2d  34427  sigapildsys  34496  ldgenpisyslem1  34497  voliune  34563  oms0  34631  rrvadd  34786  ballotlem7  34870  breprexplema  34961  cvmcov  35653  rdgssun  37911  exrecfnlem  37912  phpreu  38142  matunitlindflem2  38155  poimirlem16  38174  poimirlem19  38177  itg2addnclem  38209  ftc1anclem5  38235  totbndbnd  38327  mzpsubmpt  43365  eq0rabdioph  43398  eqrabdioph  43399  aomclem8  43679  binomcxplemdvbinom  44954  binomcxplemdvsum  44956  binomcxplemnotnn0  44957  refsumcn  45641  refsum2cnlem1  45648  disjrnmpt2  45797  disjf1o  45800  disjinfi  45801  choicefi  45808  axccdom  45829  rnmptbd2lem  45854  infnsuprnmpt  45856  rnmptbdlem  45861  rnmptss2  45863  rnmptssbi  45866  supxrleubrnmpt  46011  suprleubrnmpt  46027  infrnmptle  46028  infxrunb3rnmpt  46033  uzub  46036  supminfrnmpt  46050  infxrgelbrnmpt  46059  infrpgernmpt  46070  supminfxrrnmpt  46076  fmuldfeqlem1  46189  fmuldfeq  46190  climneg  46217  climdivf  46219  mullimc  46223  idlimc  46233  sumnnodd  46237  neglimc  46252  addlimc  46253  0ellimcdiv  46254  fnlimfvre  46279  fnlimabslt  46284  climreclmpt  46289  climfveqmpt2  46298  climeldmeqmpt2  46300  climeqmpt  46302  limsupubuz  46318  climinfmpt  46320  limsupubuzmpt  46324  limsupequzmptlem  46333  limsupre2mpt  46335  limsupre3mpt  46339  limsupreuzmpt  46344  liminflelimsuplem  46380  liminfvalxr  46388  liminfvalxrmpt  46391  liminfltlem  46409  liminflbuz2  46420  liminfpnfuz  46421  xlimmnfmpt  46448  xlimpnfmpt  46449  xlimpnfxnegmnf2  46463  cncfmptssg  46476  cncfshift  46479  cncficcgt0  46493  cncfiooicclem1  46498  dvnmul  46548  dvmptfprod  46550  itgsin0pilem1  46555  ibliccsinexp  46556  itgsinexplem1  46559  itgsinexp  46560  iblspltprt  46578  itgsubsticclem  46580  stoweidlem16  46621  stoweidlem18  46623  stoweidlem19  46624  stoweidlem20  46625  stoweidlem22  46627  stoweidlem23  46628  stoweidlem27  46632  stoweidlem31  46636  stoweidlem32  46637  stoweidlem34  46639  stoweidlem35  46640  stoweidlem36  46641  stoweidlem40  46645  stoweidlem41  46646  stoweidlem42  46647  stoweidlem43  46648  stoweidlem44  46649  stoweidlem45  46650  stoweidlem48  46653  stoweidlem51  46656  stoweidlem55  46660  stoweidlem59  46664  stoweidlem60  46665  stoweidlem62  46667  wallispilem5  46674  stirlinglem4  46682  stirlinglem5  46683  stirlinglem8  46686  stirlinglem11  46689  stirlinglem12  46690  stirlinglem13  46691  stirlinglem14  46692  stirlinglem15  46693  stirling  46694  fourierdlem16  46728  fourierdlem21  46733  fourierdlem22  46734  fourierdlem68  46779  fourierdlem73  46784  fourierdlem80  46791  fourierdlem89  46800  fourierdlem91  46802  fourierdlem93  46804  fourierdlem103  46814  fourierdlem104  46815  fourierdlem112  46823  fourierdlem115  46826  fourierd  46827  fourierclimd  46828  etransclem48  46887  sge00  46981  sge0revalmpt  46983  sge0f1o  46987  sge0fsummpt  46995  sge0gerp  47000  sge0pnffigt  47001  sge0lefi  47003  sge0ltfirp  47005  sge0resplit  47011  sge0iunmptlemfi  47018  sge0iunmpt  47023  sge0xadd  47040  sge0fsummptf  47041  sge0gtfsumgt  47048  sge0reuz  47052  iundjiun  47065  meaiuninc3v  47089  omeiunltfirp  47124  omeiunlempt  47125  hoicvrrex  47161  ovncvrrp  47169  ovnhoilem1  47206  ovnlecvr2  47215  opnvonmbllem1  47237  iunhoiioolem  47280  smfpimltmpt  47351  issmfdmpt  47353  smfconst  47354  smfpimltxrmptf  47363  smflimlem2  47377  smflim  47382  smfpimgtmpt  47386  smfpimgtxrmptf  47389  smfpimcclem  47412  smfpimcc  47413  smflimmpt  47415  smfsupmpt  47420  smfsupxr  47421  smfinfmpt  47424  smflimsuplem2  47426  smflimsuplem7  47431  smflimsupmpt  47434  smfliminfmpt  47437  cfsetsnfsetf  47683  1arymaptfo  49307  2arymaptfo  49318  setrec2mpt  50359  aacllem  50474