Theorem nfmpt1 5171

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

Syntax hints:   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Ⅎwnfc 2886  {copab 5134   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-opab 5135  df-mpt 5154

This theorem is referenced by:  nffvmpt1  6838  fvmptss  6948  fvmptd3f  6951  mpteqb  6955  fvmptf  6957  ralrnmptw  7035  ralrnmpt  7037  f1ompt  7052  fompt  7059  f1mpt  7205  fliftfun  7256  rdgsucmptf  8357  rdgsucmptnf  8358  frsucmpt  8367  frsucmptn  8368  dom2lem  8929  mapxpen  9071  cnfcom3clem  9617  ttrclselem1  9637  ttrclselem2  9638  infxpenc2lem2  9933  dfac8clem  9945  acnlem  9961  fin23lem32  10257  axcc3  10351  ac6num  10392  nfcprod1  15864  yonedalem4b  18233  prdsgsum  19947  pwsgprod  20300  cayleyhamilton1  22875  neiptopreu  23116  2ndcdisj  23439  ptcnp  23605  cnmpt11  23646  cnmptk2  23669  xkocnv  23797  utopsnneiplem  24230  restmetu  24553  mbfposr  25637  mbfsup  25649  itg1climres  25699  itg2splitlem  25733  itg2split  25734  itg2cnlem1  25746  nfitg1  25759  dvlipcn  25979  lhop2  26000  dvfsumabs  26008  itgparts  26032  itgsubstlem  26033  itgulm2  26392  lgamgulm2  27017  lgseisenlem2  27357  istrkg2ld  28546  cnlnadjlem5  32160  acunirnmpt2  32752  acunirnmpt2f  32753  aciunf1lem  32754  ofpreima  32757  fnpreimac  32762  disjdsct  32795  fpwrelmap  32825  prodindf  32941  suppgsumssiun  33153  elrgspnsubrunlem2  33329  nsgqusf1olem1  33496  nsgqusf1olem3  33498  elrspunidl  33511  deg1prod  33666  mplvrpmga  33729  esplyfval1  33757  fedgmullem2  33814  locfinreflem  34024  nfesum1  34224  esumc  34235  esumrnmpt2  34252  esumsup  34273  esumgect  34274  esum2d  34277  sigapildsys  34346  ldgenpisyslem1  34347  voliune  34413  oms0  34481  rrvadd  34636  ballotlem7  34720  breprexplema  34814  cvmcov  35491  rdgssun  37740  exrecfnlem  37741  phpreu  37971  matunitlindflem2  37984  poimirlem16  38003  poimirlem19  38006  itg2addnclem  38038  ftc1anclem5  38064  totbndbnd  38156  mzpsubmpt  43192  eq0rabdioph  43225  eqrabdioph  43226  aomclem8  43506  binomcxplemdvbinom  44797  binomcxplemdvsum  44799  binomcxplemnotnn0  44800  refsumcn  45478  refsum2cnlem1  45485  disjrnmpt2  45635  disjf1o  45638  disjinfi  45639  choicefi  45646  axccdom  45667  rnmptbd2lem  45692  infnsuprnmpt  45694  rnmptbdlem  45699  rnmptss2  45701  rnmptssbi  45704  supxrleubrnmpt  45849  suprleubrnmpt  45865  infrnmptle  45866  infxrunb3rnmpt  45871  uzub  45874  supminfrnmpt  45888  infxrgelbrnmpt  45897  infrpgernmpt  45908  supminfxrrnmpt  45914  fmuldfeqlem1  46027  fmuldfeq  46028  climneg  46055  climdivf  46057  mullimc  46061  idlimc  46071  sumnnodd  46075  neglimc  46090  addlimc  46091  0ellimcdiv  46092  fnlimfvre  46117  fnlimabslt  46122  climreclmpt  46127  climfveqmpt2  46136  climeldmeqmpt2  46138  climeqmpt  46140  limsupubuz  46156  climinfmpt  46158  limsupubuzmpt  46162  limsupequzmptlem  46171  limsupre2mpt  46173  limsupre3mpt  46177  limsupreuzmpt  46182  liminflelimsuplem  46218  liminfvalxr  46226  liminfvalxrmpt  46229  liminfltlem  46247  liminflbuz2  46258  liminfpnfuz  46259  xlimmnfmpt  46286  xlimpnfmpt  46287  xlimpnfxnegmnf2  46301  cncfmptssg  46314  cncfshift  46317  cncficcgt0  46331  cncfiooicclem1  46336  dvnmul  46386  dvmptfprod  46388  itgsin0pilem1  46393  ibliccsinexp  46394  itgsinexplem1  46397  itgsinexp  46398  iblspltprt  46416  itgsubsticclem  46418  stoweidlem16  46459  stoweidlem18  46461  stoweidlem19  46462  stoweidlem20  46463  stoweidlem22  46465  stoweidlem23  46466  stoweidlem27  46470  stoweidlem31  46474  stoweidlem32  46475  stoweidlem34  46477  stoweidlem35  46478  stoweidlem36  46479  stoweidlem40  46483  stoweidlem41  46484  stoweidlem42  46485  stoweidlem43  46486  stoweidlem44  46487  stoweidlem45  46488  stoweidlem48  46491  stoweidlem51  46494  stoweidlem55  46498  stoweidlem59  46502  stoweidlem60  46503  stoweidlem62  46505  wallispilem5  46512  stirlinglem4  46520  stirlinglem5  46521  stirlinglem8  46524  stirlinglem11  46527  stirlinglem12  46528  stirlinglem13  46529  stirlinglem14  46530  stirlinglem15  46531  stirling  46532  fourierdlem16  46566  fourierdlem21  46571  fourierdlem22  46572  fourierdlem68  46617  fourierdlem73  46622  fourierdlem80  46629  fourierdlem89  46638  fourierdlem91  46640  fourierdlem93  46642  fourierdlem103  46652  fourierdlem104  46653  fourierdlem112  46661  fourierdlem115  46664  fourierd  46665  fourierclimd  46666  etransclem48  46725  sge00  46819  sge0revalmpt  46821  sge0f1o  46825  sge0fsummpt  46833  sge0gerp  46838  sge0pnffigt  46839  sge0lefi  46841  sge0ltfirp  46843  sge0resplit  46849  sge0iunmptlemfi  46856  sge0iunmpt  46861  sge0xadd  46878  sge0fsummptf  46879  sge0gtfsumgt  46886  sge0reuz  46890  iundjiun  46903  meaiuninc3v  46927  omeiunltfirp  46962  omeiunlempt  46963  hoicvrrex  46999  ovncvrrp  47007  ovnhoilem1  47044  ovnlecvr2  47053  opnvonmbllem1  47075  iunhoiioolem  47118  smfpimltmpt  47189  issmfdmpt  47191  smfconst  47192  smfpimltxrmptf  47201  smflimlem2  47215  smflim  47220  smfpimgtmpt  47224  smfpimgtxrmptf  47227  smfpimcclem  47250  smfpimcc  47251  smflimmpt  47253  smfsupmpt  47258  smfsupxr  47259  smfinfmpt  47262  smflimsuplem2  47264  smflimsuplem7  47269  smflimsupmpt  47272  smfliminfmpt  47275  cfsetsnfsetf  47521  1arymaptfo  49134  2arymaptfo  49145  setrec2mpt  50187  aacllem  50291