Theorem nfmpt1 4675

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

Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Ⅎwnfc 2738  {copab 4642   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-opab 4644  df-mpt 4645

This theorem is referenced by:  nffvmpt1  6111  fvmptss  6201  fvmptdf  6204  mpteqb  6207  fvmptf  6209  ralrnmpt  6276  f1ompt  6290  f1mpt  6419  fliftfun  6462  rdgsucmptf  7411  rdgsucmptnf  7412  frsucmpt  7420  frsucmptn  7421  dom2lem  7881  mapxpen  8011  cnfcom3clem  8485  infxpenc2lem2  8726  dfac8clem  8738  acnlem  8754  fin23lem32  9049  axcc3  9143  ac6num  9184  nfcprod1  14479  yonedalem4b  16739  prdsgsum  18200  cayleyhamilton1  20516  neiptopreu  20747  2ndcdisj  21069  ptcnp  21235  cnmpt11  21276  cnmptk2  21299  xkocnv  21427  utopsnneiplem  21861  restmetu  22185  mbfposr  23225  mbfsup  23237  itg1climres  23287  itg2splitlem  23321  itg2split  23322  itg2cnlem1  23334  nfitg1  23346  dvlipcn  23561  lhop2  23582  dvfsumabs  23590  itgparts  23614  itgsubstlem  23615  itgulm2  23967  lgamgulm2  24562  lgseisenlem2  24901  istrkg2ld  25159  cnlnadjlem5  28314  acunirnmpt2  28842  acunirnmpt2f  28843  aciunf1lem  28844  ofpreima  28848  disjdsct  28863  fpwrelmap  28896  locfinreflem  29235  nfesum1  29429  esumc  29440  esumrnmpt2  29457  esumsup  29478  esumgect  29479  esum2d  29482  sigapildsys  29552  ldgenpisyslem1  29553  voliune  29619  oms0  29686  rrvadd  29841  ballotlem7  29924  cvmcov  30499  trpredlem1  30971  trpredrec  30982  phpreu  32563  matunitlindflem2  32576  poimirlem16  32595  poimirlem19  32598  itg2addnclem  32631  ftc1anclem5  32659  totbndbnd  32758  mzpsubmpt  36324  eq0rabdioph  36358  eqrabdioph  36359  aomclem8  36649  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  refsumcn  38212  refsum2cnlem1  38219  suprnmpt  38350  wessf1ornlem  38366  disjrnmpt2  38370  disjf1o  38373  fompt  38374  disjinfi  38375  choicefi  38387  axccdom  38411  fmuldfeqlem1  38649  fmuldfeq  38650  climneg  38677  climdivf  38679  mullimc  38683  idlimc  38693  sumnnodd  38697  neglimc  38714  addlimc  38715  0ellimcdiv  38716  fnlimfvre  38741  fnlimabslt  38746  cncfmptssg  38755  cncfshift  38759  cncficcgt0  38774  cncfiooicclem1  38779  dvnmul  38833  dvmptfprod  38835  itgsin0pilem1  38841  ibliccsinexp  38842  itgsinexplem1  38845  itgsinexp  38846  iblspltprt  38865  itgsubsticclem  38867  stoweidlem16  38909  stoweidlem18  38911  stoweidlem19  38912  stoweidlem20  38913  stoweidlem22  38915  stoweidlem23  38916  stoweidlem27  38920  stoweidlem31  38924  stoweidlem32  38925  stoweidlem34  38927  stoweidlem35  38928  stoweidlem36  38929  stoweidlem40  38933  stoweidlem41  38934  stoweidlem42  38935  stoweidlem43  38936  stoweidlem44  38937  stoweidlem45  38938  stoweidlem48  38941  stoweidlem51  38944  stoweidlem55  38948  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  wallispilem5  38962  stirlinglem4  38970  stirlinglem5  38971  stirlinglem8  38974  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  stirling  38982  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem53  39052  fourierdlem68  39067  fourierdlem73  39072  fourierdlem80  39079  fourierdlem89  39088  fourierdlem91  39090  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem115  39114  fourierd  39115  fourierclimd  39116  etransclem48  39175  sge00  39269  sge0revalmpt  39271  sge0f1o  39275  sge0fsummpt  39283  sge0gerp  39288  sge0pnffigt  39289  sge0lefi  39291  sge0ltfirp  39293  sge0resplit  39299  sge0iunmptlemfi  39306  sge0iunmpt  39311  sge0xadd  39328  sge0fsummptf  39329  sge0gtfsumgt  39336  sge0reuz  39340  iundjiun  39353  omeiunltfirp  39409  omeiunlempt  39410  hoicvrrex  39446  ovncvrrp  39454  ovnhoilem1  39491  ovnlecvr2  39500  opnvonmbllem1  39522  iunhoiioolem  39566  pimgtmnf  39609  smfpimltmpt  39633  issmfdmpt  39635  smfconst  39636  smfpimltxrmpt  39645  smflimlem2  39658  smflim  39663  smfpimgtmpt  39667  smfpimgtxrmpt  39670  aacllem  42356