Theorem nfmpt1 5256

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Ⅎwnfc 2883  {copab 5210   ↦ cmpt 5231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-opab 5211  df-mpt 5232

This theorem is referenced by:  nffvmpt1  6902  fvmptss  7010  fvmptd3f  7013  mpteqb  7017  fvmptf  7019  ralrnmptw  7095  ralrnmpt  7097  f1ompt  7112  fompt  7119  f1mpt  7262  fliftfun  7311  rdgsucmptf  8430  rdgsucmptnf  8431  frsucmpt  8440  frsucmptn  8441  dom2lem  8990  mapxpen  9145  cnfcom3clem  9702  ttrclselem1  9722  ttrclselem2  9723  infxpenc2lem2  10017  dfac8clem  10029  acnlem  10045  fin23lem32  10341  axcc3  10435  ac6num  10476  nfcprod1  15858  yonedalem4b  18233  prdsgsum  19890  cayleyhamilton1  22614  neiptopreu  22857  2ndcdisj  23180  ptcnp  23346  cnmpt11  23387  cnmptk2  23410  xkocnv  23538  utopsnneiplem  23972  restmetu  24299  mbfposr  25393  mbfsup  25405  itg1climres  25456  itg2splitlem  25490  itg2split  25491  itg2cnlem1  25503  nfitg1  25515  dvlipcn  25735  lhop2  25756  dvfsumabs  25764  itgparts  25788  itgsubstlem  25789  itgulm2  26145  lgamgulm2  26764  lgseisenlem2  27103  istrkg2ld  27966  cnlnadjlem5  31579  acunirnmpt2  32140  acunirnmpt2f  32141  aciunf1lem  32142  ofpreima  32145  fnpreimac  32151  disjdsct  32179  fpwrelmap  32213  nsgqusf1olem1  32786  nsgqusf1olem3  32788  elrspunidl  32808  fedgmullem2  32991  locfinreflem  33106  prodindf  33307  nfesum1  33324  esumc  33335  esumrnmpt2  33352  esumsup  33373  esumgect  33374  esum2d  33377  sigapildsys  33446  ldgenpisyslem1  33447  voliune  33513  oms0  33582  rrvadd  33737  ballotlem7  33820  breprexplema  33928  cvmcov  34540  rdgssun  36562  exrecfnlem  36563  phpreu  36775  matunitlindflem2  36788  poimirlem16  36807  poimirlem19  36810  itg2addnclem  36842  ftc1anclem5  36868  totbndbnd  36960  pwsgprod  41416  mzpsubmpt  41783  eq0rabdioph  41816  eqrabdioph  41817  aomclem8  42105  binomcxplemdvbinom  43414  binomcxplemdvsum  43416  binomcxplemnotnn0  43417  refsumcn  44016  refsum2cnlem1  44023  disjrnmpt2  44186  disjf1o  44189  disjinfi  44190  choicefi  44198  axccdom  44220  rnmptbd2lem  44251  infnsuprnmpt  44253  rnmptbdlem  44258  rnmptss2  44260  rnmptssbi  44264  supxrleubrnmpt  44415  suprleubrnmpt  44431  infrnmptle  44432  infxrunb3rnmpt  44437  uzub  44440  supminfrnmpt  44454  infxrgelbrnmpt  44463  infrpgernmpt  44474  supminfxrrnmpt  44480  fmuldfeqlem1  44597  fmuldfeq  44598  climneg  44625  climdivf  44627  mullimc  44631  idlimc  44641  sumnnodd  44645  neglimc  44662  addlimc  44663  0ellimcdiv  44664  fnlimfvre  44689  fnlimabslt  44694  climreclmpt  44699  climfveqmpt2  44708  climeldmeqmpt2  44710  climeqmpt  44712  limsupubuz  44728  climinfmpt  44730  limsupubuzmpt  44734  limsupequzmptlem  44743  limsupre2mpt  44745  limsupre3mpt  44749  limsupreuzmpt  44754  liminflelimsuplem  44790  liminfvalxr  44798  liminfvalxrmpt  44801  liminfltlem  44819  liminflbuz2  44830  liminfpnfuz  44831  xlimmnfmpt  44858  xlimpnfmpt  44859  xlimpnfxnegmnf2  44873  cncfmptssg  44886  cncfshift  44889  cncficcgt0  44903  cncfiooicclem1  44908  dvnmul  44958  dvmptfprod  44960  itgsin0pilem1  44965  ibliccsinexp  44966  itgsinexplem1  44969  itgsinexp  44970  iblspltprt  44988  itgsubsticclem  44990  stoweidlem16  45031  stoweidlem18  45033  stoweidlem19  45034  stoweidlem20  45035  stoweidlem22  45037  stoweidlem23  45038  stoweidlem27  45042  stoweidlem31  45046  stoweidlem32  45047  stoweidlem34  45049  stoweidlem35  45050  stoweidlem36  45051  stoweidlem40  45055  stoweidlem41  45056  stoweidlem42  45057  stoweidlem43  45058  stoweidlem44  45059  stoweidlem45  45060  stoweidlem48  45063  stoweidlem51  45066  stoweidlem55  45070  stoweidlem59  45074  stoweidlem60  45075  stoweidlem62  45077  wallispilem5  45084  stirlinglem4  45092  stirlinglem5  45093  stirlinglem8  45096  stirlinglem11  45099  stirlinglem12  45100  stirlinglem13  45101  stirlinglem14  45102  stirlinglem15  45103  stirling  45104  fourierdlem16  45138  fourierdlem21  45143  fourierdlem22  45144  fourierdlem68  45189  fourierdlem73  45194  fourierdlem80  45201  fourierdlem89  45210  fourierdlem91  45212  fourierdlem93  45214  fourierdlem103  45224  fourierdlem104  45225  fourierdlem112  45233  fourierdlem115  45236  fourierd  45237  fourierclimd  45238  etransclem48  45297  sge00  45391  sge0revalmpt  45393  sge0f1o  45397  sge0fsummpt  45405  sge0gerp  45410  sge0pnffigt  45411  sge0lefi  45413  sge0ltfirp  45415  sge0resplit  45421  sge0iunmptlemfi  45428  sge0iunmpt  45433  sge0xadd  45450  sge0fsummptf  45451  sge0gtfsumgt  45458  sge0reuz  45462  iundjiun  45475  meaiuninc3v  45499  omeiunltfirp  45534  omeiunlempt  45535  hoicvrrex  45571  ovncvrrp  45579  ovnhoilem1  45616  ovnlecvr2  45625  opnvonmbllem1  45647  iunhoiioolem  45690  smfpimltmpt  45761  issmfdmpt  45763  smfconst  45764  smfpimltxrmptf  45773  smflimlem2  45787  smflim  45792  smfpimgtmpt  45796  smfpimgtxrmptf  45799  smfpimcclem  45822  smfpimcc  45823  smflimmpt  45825  smfsupmpt  45830  smfsupxr  45831  smfinfmpt  45834  smflimsuplem2  45836  smflimsuplem7  45841  smflimsupmpt  45844  smfliminfmpt  45847  cfsetsnfsetf  46067  1arymaptfo  47417  2arymaptfo  47428  setrec2mpt  47830  aacllem  47936