Theorem nfmpt1 5178

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Ⅎwnfc 2886  {copab 5132   ↦ cmpt 5153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-opab 5133  df-mpt 5154

This theorem is referenced by:  nffvmpt1  6767  fvmptss  6869  fvmptd3f  6872  mpteqb  6876  fvmptf  6878  ralrnmptw  6952  ralrnmpt  6954  f1ompt  6967  f1mpt  7115  fliftfun  7163  rdgsucmptf  8230  rdgsucmptnf  8231  frsucmpt  8239  frsucmptn  8240  dom2lem  8735  mapxpen  8879  cnfcom3clem  9393  trpredlem1  9405  trpredrec  9415  infxpenc2lem2  9707  dfac8clem  9719  acnlem  9735  fin23lem32  10031  axcc3  10125  ac6num  10166  nfcprod1  15548  yonedalem4b  17910  prdsgsum  19497  cayleyhamilton1  21949  neiptopreu  22192  2ndcdisj  22515  ptcnp  22681  cnmpt11  22722  cnmptk2  22745  xkocnv  22873  utopsnneiplem  23307  restmetu  23632  mbfposr  24721  mbfsup  24733  itg1climres  24784  itg2splitlem  24818  itg2split  24819  itg2cnlem1  24831  nfitg1  24843  dvlipcn  25063  lhop2  25084  dvfsumabs  25092  itgparts  25116  itgsubstlem  25117  itgulm2  25473  lgamgulm2  26090  lgseisenlem2  26429  istrkg2ld  26725  cnlnadjlem5  30334  acunirnmpt2  30899  acunirnmpt2f  30900  aciunf1lem  30901  ofpreima  30904  fnpreimac  30910  disjdsct  30937  fpwrelmap  30970  nsgqusf1olem1  31500  nsgqusf1olem3  31502  elrspunidl  31508  fedgmullem2  31613  locfinreflem  31692  prodindf  31891  nfesum1  31908  esumc  31919  esumrnmpt2  31936  esumsup  31957  esumgect  31958  esum2d  31961  sigapildsys  32030  ldgenpisyslem1  32031  voliune  32097  oms0  32164  rrvadd  32319  ballotlem7  32402  breprexplema  32510  cvmcov  33125  ttrclselem1  33711  ttrclselem2  33712  rdgssun  35476  exrecfnlem  35477  phpreu  35688  matunitlindflem2  35701  poimirlem16  35720  poimirlem19  35723  itg2addnclem  35755  ftc1anclem5  35781  totbndbnd  35874  pwsgprod  40194  mzpsubmpt  40481  eq0rabdioph  40514  eqrabdioph  40515  aomclem8  40802  binomcxplemdvbinom  41860  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  refsumcn  42462  refsum2cnlem1  42469  disjrnmpt2  42615  disjf1o  42618  fompt  42619  disjinfi  42620  choicefi  42629  axccdom  42651  rnmptbd2lem  42683  infnsuprnmpt  42685  rnmptbdlem  42690  rnmptss2  42692  rnmptssbi  42696  supxrleubrnmpt  42836  suprleubrnmpt  42852  infrnmptle  42853  infxrunb3rnmpt  42858  uzub  42861  supminfrnmpt  42875  infxrgelbrnmpt  42884  infrpgernmpt  42895  supminfxrrnmpt  42901  fmuldfeqlem1  43013  fmuldfeq  43014  climneg  43041  climdivf  43043  mullimc  43047  idlimc  43057  sumnnodd  43061  neglimc  43078  addlimc  43079  0ellimcdiv  43080  fnlimfvre  43105  fnlimabslt  43110  climreclmpt  43115  climfveqmpt2  43124  climeldmeqmpt2  43126  climeqmpt  43128  limsupubuz  43144  climinfmpt  43146  limsupubuzmpt  43150  limsupequzmptlem  43159  limsupre2mpt  43161  limsupre3mpt  43165  limsupreuzmpt  43170  liminflelimsuplem  43206  liminfvalxr  43214  liminfvalxrmpt  43217  liminfltlem  43235  liminflbuz2  43246  liminfpnfuz  43247  xlimmnfmpt  43274  xlimpnfmpt  43275  xlimpnfxnegmnf2  43289  cncfmptssg  43302  cncfshift  43305  cncficcgt0  43319  cncfiooicclem1  43324  dvnmul  43374  dvmptfprod  43376  itgsin0pilem1  43381  ibliccsinexp  43382  itgsinexplem1  43385  itgsinexp  43386  iblspltprt  43404  itgsubsticclem  43406  stoweidlem16  43447  stoweidlem18  43449  stoweidlem19  43450  stoweidlem20  43451  stoweidlem22  43453  stoweidlem23  43454  stoweidlem27  43458  stoweidlem31  43462  stoweidlem32  43463  stoweidlem34  43465  stoweidlem35  43466  stoweidlem36  43467  stoweidlem40  43471  stoweidlem41  43472  stoweidlem42  43473  stoweidlem43  43474  stoweidlem44  43475  stoweidlem45  43476  stoweidlem48  43479  stoweidlem51  43482  stoweidlem55  43486  stoweidlem59  43490  stoweidlem60  43491  stoweidlem62  43493  wallispilem5  43500  stirlinglem4  43508  stirlinglem5  43509  stirlinglem8  43512  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  stirling  43520  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem68  43605  fourierdlem73  43610  fourierdlem80  43617  fourierdlem89  43626  fourierdlem91  43628  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  fourierdlem112  43649  fourierdlem115  43652  fourierd  43653  fourierclimd  43654  etransclem48  43713  sge00  43804  sge0revalmpt  43806  sge0f1o  43810  sge0fsummpt  43818  sge0gerp  43823  sge0pnffigt  43824  sge0lefi  43826  sge0ltfirp  43828  sge0resplit  43834  sge0iunmptlemfi  43841  sge0iunmpt  43846  sge0xadd  43863  sge0fsummptf  43864  sge0gtfsumgt  43871  sge0reuz  43875  iundjiun  43888  meaiuninc3v  43912  omeiunltfirp  43947  omeiunlempt  43948  hoicvrrex  43984  ovncvrrp  43992  ovnhoilem1  44029  ovnlecvr2  44038  opnvonmbllem1  44060  iunhoiioolem  44103  pimgtmnf  44146  smfpimltmpt  44169  issmfdmpt  44171  smfconst  44172  smfpimltxrmpt  44181  smflimlem2  44194  smflim  44199  smfpimgtmpt  44203  smfpimgtxrmpt  44206  smfpimcclem  44227  smfpimcc  44228  smflimmpt  44230  smfsupmpt  44235  smfsupxr  44236  smfinfmpt  44239  smflimsuplem2  44241  smflimsuplem7  44246  smflimsupmpt  44249  smfliminfmpt  44252  cfsetsnfsetf  44439  1arymaptfo  45877  2arymaptfo  45888  aacllem  46391