Theorem nfmpt1 5197

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Ⅎwnfc 2883  {copab 5160   ↦ cmpt 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-opab 5161  df-mpt 5180

This theorem is referenced by:  nffvmpt1  6845  fvmptss  6953  fvmptd3f  6956  mpteqb  6960  fvmptf  6962  ralrnmptw  7039  ralrnmpt  7041  f1ompt  7056  fompt  7063  f1mpt  7207  fliftfun  7258  rdgsucmptf  8359  rdgsucmptnf  8360  frsucmpt  8369  frsucmptn  8370  dom2lem  8929  mapxpen  9071  cnfcom3clem  9614  ttrclselem1  9634  ttrclselem2  9635  infxpenc2lem2  9930  dfac8clem  9942  acnlem  9958  fin23lem32  10254  axcc3  10348  ac6num  10389  nfcprod1  15831  yonedalem4b  18199  prdsgsum  19910  pwsgprod  20265  cayleyhamilton1  22836  neiptopreu  23077  2ndcdisj  23400  ptcnp  23566  cnmpt11  23607  cnmptk2  23630  xkocnv  23758  utopsnneiplem  24191  restmetu  24514  mbfposr  25609  mbfsup  25621  itg1climres  25671  itg2splitlem  25705  itg2split  25706  itg2cnlem1  25718  nfitg1  25731  dvlipcn  25955  lhop2  25976  dvfsumabs  25985  itgparts  26010  itgsubstlem  26011  itgulm2  26374  lgamgulm2  27002  lgseisenlem2  27343  istrkg2ld  28532  cnlnadjlem5  32146  acunirnmpt2  32738  acunirnmpt2f  32739  aciunf1lem  32740  ofpreima  32743  fnpreimac  32749  disjdsct  32782  fpwrelmap  32812  prodindf  32944  elrgspnsubrunlem2  33330  nsgqusf1olem1  33494  nsgqusf1olem3  33496  elrspunidl  33509  deg1prod  33664  mplvrpmga  33710  fedgmullem2  33787  locfinreflem  33997  nfesum1  34197  esumc  34208  esumrnmpt2  34225  esumsup  34246  esumgect  34247  esum2d  34250  sigapildsys  34319  ldgenpisyslem1  34320  voliune  34386  oms0  34454  rrvadd  34609  ballotlem7  34693  breprexplema  34787  cvmcov  35457  rdgssun  37583  exrecfnlem  37584  phpreu  37805  matunitlindflem2  37818  poimirlem16  37837  poimirlem19  37840  itg2addnclem  37872  ftc1anclem5  37898  totbndbnd  37990  mzpsubmpt  42985  eq0rabdioph  43018  eqrabdioph  43019  aomclem8  43303  binomcxplemdvbinom  44594  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  refsumcn  45275  refsum2cnlem1  45282  disjrnmpt2  45432  disjf1o  45435  disjinfi  45436  choicefi  45444  axccdom  45466  rnmptbd2lem  45492  infnsuprnmpt  45494  rnmptbdlem  45499  rnmptss2  45501  rnmptssbi  45504  supxrleubrnmpt  45650  suprleubrnmpt  45666  infrnmptle  45667  infxrunb3rnmpt  45672  uzub  45675  supminfrnmpt  45689  infxrgelbrnmpt  45698  infrpgernmpt  45709  supminfxrrnmpt  45715  fmuldfeqlem1  45828  fmuldfeq  45829  climneg  45856  climdivf  45858  mullimc  45862  idlimc  45872  sumnnodd  45876  neglimc  45891  addlimc  45892  0ellimcdiv  45893  fnlimfvre  45918  fnlimabslt  45923  climreclmpt  45928  climfveqmpt2  45937  climeldmeqmpt2  45939  climeqmpt  45941  limsupubuz  45957  climinfmpt  45959  limsupubuzmpt  45963  limsupequzmptlem  45972  limsupre2mpt  45974  limsupre3mpt  45978  limsupreuzmpt  45983  liminflelimsuplem  46019  liminfvalxr  46027  liminfvalxrmpt  46030  liminfltlem  46048  liminflbuz2  46059  liminfpnfuz  46060  xlimmnfmpt  46087  xlimpnfmpt  46088  xlimpnfxnegmnf2  46102  cncfmptssg  46115  cncfshift  46118  cncficcgt0  46132  cncfiooicclem1  46137  dvnmul  46187  dvmptfprod  46189  itgsin0pilem1  46194  ibliccsinexp  46195  itgsinexplem1  46198  itgsinexp  46199  iblspltprt  46217  itgsubsticclem  46219  stoweidlem16  46260  stoweidlem18  46262  stoweidlem19  46263  stoweidlem20  46264  stoweidlem22  46266  stoweidlem23  46267  stoweidlem27  46271  stoweidlem31  46275  stoweidlem32  46276  stoweidlem34  46278  stoweidlem35  46279  stoweidlem36  46280  stoweidlem40  46284  stoweidlem41  46285  stoweidlem42  46286  stoweidlem43  46287  stoweidlem44  46288  stoweidlem45  46289  stoweidlem48  46292  stoweidlem51  46295  stoweidlem55  46299  stoweidlem59  46303  stoweidlem60  46304  stoweidlem62  46306  wallispilem5  46313  stirlinglem4  46321  stirlinglem5  46322  stirlinglem8  46325  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  stirling  46333  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem68  46418  fourierdlem73  46423  fourierdlem80  46430  fourierdlem89  46439  fourierdlem91  46441  fourierdlem93  46443  fourierdlem103  46453  fourierdlem104  46454  fourierdlem112  46462  fourierdlem115  46465  fourierd  46466  fourierclimd  46467  etransclem48  46526  sge00  46620  sge0revalmpt  46622  sge0f1o  46626  sge0fsummpt  46634  sge0gerp  46639  sge0pnffigt  46640  sge0lefi  46642  sge0ltfirp  46644  sge0resplit  46650  sge0iunmptlemfi  46657  sge0iunmpt  46662  sge0xadd  46679  sge0fsummptf  46680  sge0gtfsumgt  46687  sge0reuz  46691  iundjiun  46704  meaiuninc3v  46728  omeiunltfirp  46763  omeiunlempt  46764  hoicvrrex  46800  ovncvrrp  46808  ovnhoilem1  46845  ovnlecvr2  46854  opnvonmbllem1  46876  iunhoiioolem  46919  smfpimltmpt  46990  issmfdmpt  46992  smfconst  46993  smfpimltxrmptf  47002  smflimlem2  47016  smflim  47021  smfpimgtmpt  47025  smfpimgtxrmptf  47028  smfpimcclem  47051  smfpimcc  47052  smflimmpt  47054  smfsupmpt  47059  smfsupxr  47060  smfinfmpt  47063  smflimsuplem2  47065  smflimsuplem7  47070  smflimsupmpt  47073  smfliminfmpt  47076  cfsetsnfsetf  47304  1arymaptfo  48889  2arymaptfo  48900  setrec2mpt  49942  aacllem  50046