Theorem nfmpt1 5210

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

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Ⅎwnfc 2910  {copab 5173   ↦ cmpt 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-opab 5174  df-mpt 5193

This theorem is referenced by:  nffvmpt1  6892  fvmptss  7002  fvmptd3f  7005  mpteqb  7009  fvmptf  7011  ralrnmptw  7089  ralrnmpt  7091  f1ompt  7106  fompt  7113  f1mpt  7259  fliftfun  7310  rdgsucmptf  8411  rdgsucmptnf  8412  frsucmpt  8421  frsucmptn  8422  dom2lem  8985  mapxpen  9127  cnfcom3clem  9670  ttrclselem1  9690  ttrclselem2  9691  infxpenc2lem2  10000  dfac8clem  10012  acnlem  10028  fin23lem32  10323  axcc3  10417  ac6num  10458  nfcprod1  15958  yonedalem4b  18327  prdsgsum  20046  pwsgprod  20407  cayleyhamilton1  23049  neiptopreu  23290  2ndcdisj  23613  ptcnp  23779  cnmpt11  23820  cnmptk2  23843  xkocnv  23971  utopsnneiplem  24404  restmetu  24727  mbfposr  25811  mbfsup  25823  itg1climres  25873  itg2splitlem  25907  itg2split  25908  itg2cnlem1  25920  nfitg1  25933  dvlipcn  26153  lhop2  26174  dvfsumabs  26182  itgparts  26206  itgsubstlem  26207  itgulm2  26572  lgamgulm2  27200  lgseisenlem2  27540  istrkg2ld  28729  cnlnadjlem5  32423  acunirnmpt2  33005  acunirnmpt2f  33006  aciunf1lem  33007  ofpreima  33010  fnpreimac  33015  disjdsct  33048  fpwrelmap  33078  prodindf  33182  suppgsumssiun  33392  elrgspnsubrunlem2  33568  nsgqusf1olem1  33722  nsgqusf1olem3  33724  elrspunidl  33736  deg1prod  33873  mplvrpmga  33935  esplyfval1  33963  fedgmullem2  34020  locfinreflem  34230  nfesum1  34430  esumc  34441  esumrnmpt2  34458  esumsup  34479  esumgect  34480  esum2d  34483  sigapildsys  34552  ldgenpisyslem1  34553  voliune  34619  oms0  34687  rrvadd  34842  ballotlem7  34926  breprexplema  35017  cvmcov  35755  rdgssun  38024  exrecfnlem  38025  phpreu  38255  matunitlindflem2  38268  poimirlem16  38287  poimirlem19  38290  itg2addnclem  38322  ftc1anclem5  38348  totbndbnd  38440  mzpsubmpt  43474  eq0rabdioph  43507  eqrabdioph  43508  aomclem8  43788  binomcxplemdvbinom  45063  binomcxplemdvsum  45065  binomcxplemnotnn0  45066  refsumcn  45750  refsum2cnlem1  45757  disjrnmpt2  45906  disjf1o  45909  disjinfi  45910  choicefi  45917  axccdom  45938  rnmptbd2lem  45963  infnsuprnmpt  45965  rnmptbdlem  45970  rnmptss2  45972  rnmptssbi  45975  supxrleubrnmpt  46120  suprleubrnmpt  46136  infrnmptle  46137  infxrunb3rnmpt  46142  uzub  46145  supminfrnmpt  46159  infxrgelbrnmpt  46168  infrpgernmpt  46179  supminfxrrnmpt  46185  fmuldfeqlem1  46298  fmuldfeq  46299  climneg  46326  climdivf  46328  mullimc  46332  idlimc  46342  sumnnodd  46346  neglimc  46361  addlimc  46362  0ellimcdiv  46363  fnlimfvre  46388  fnlimabslt  46393  climreclmpt  46398  climfveqmpt2  46407  climeldmeqmpt2  46409  climeqmpt  46411  limsupubuz  46427  climinfmpt  46429  limsupubuzmpt  46433  limsupequzmptlem  46442  limsupre2mpt  46444  limsupre3mpt  46448  limsupreuzmpt  46453  liminflelimsuplem  46489  liminfvalxr  46497  liminfvalxrmpt  46500  liminfltlem  46518  liminflbuz2  46529  liminfpnfuz  46530  xlimmnfmpt  46557  xlimpnfmpt  46558  xlimpnfxnegmnf2  46572  cncfmptssg  46585  cncfshift  46588  cncficcgt0  46602  cncfiooicclem1  46607  dvnmul  46657  dvmptfprod  46659  itgsin0pilem1  46664  ibliccsinexp  46665  itgsinexplem1  46668  itgsinexp  46669  iblspltprt  46687  itgsubsticclem  46689  stoweidlem16  46730  stoweidlem18  46732  stoweidlem19  46733  stoweidlem20  46734  stoweidlem22  46736  stoweidlem23  46737  stoweidlem27  46741  stoweidlem31  46745  stoweidlem32  46746  stoweidlem34  46748  stoweidlem35  46749  stoweidlem36  46750  stoweidlem40  46754  stoweidlem41  46755  stoweidlem42  46756  stoweidlem43  46757  stoweidlem44  46758  stoweidlem45  46759  stoweidlem48  46762  stoweidlem51  46765  stoweidlem55  46769  stoweidlem59  46773  stoweidlem60  46774  stoweidlem62  46776  wallispilem5  46783  stirlinglem4  46791  stirlinglem5  46792  stirlinglem8  46795  stirlinglem11  46798  stirlinglem12  46799  stirlinglem13  46800  stirlinglem14  46801  stirlinglem15  46802  stirling  46803  fourierdlem16  46837  fourierdlem21  46842  fourierdlem22  46843  fourierdlem68  46888  fourierdlem73  46893  fourierdlem80  46900  fourierdlem89  46909  fourierdlem91  46911  fourierdlem93  46913  fourierdlem103  46923  fourierdlem104  46924  fourierdlem112  46932  fourierdlem115  46935  fourierd  46936  fourierclimd  46937  etransclem48  46996  sge00  47090  sge0revalmpt  47092  sge0f1o  47096  sge0fsummpt  47104  sge0gerp  47109  sge0pnffigt  47110  sge0lefi  47112  sge0ltfirp  47114  sge0resplit  47120  sge0iunmptlemfi  47127  sge0iunmpt  47132  sge0xadd  47149  sge0fsummptf  47150  sge0gtfsumgt  47157  sge0reuz  47161  iundjiun  47174  meaiuninc3v  47198  omeiunltfirp  47233  omeiunlempt  47234  hoicvrrex  47270  ovncvrrp  47278  ovnhoilem1  47315  ovnlecvr2  47324  opnvonmbllem1  47346  iunhoiioolem  47389  smfpimltmpt  47460  issmfdmpt  47462  smfconst  47463  smfpimltxrmptf  47472  smflimlem2  47486  smflim  47491  smfpimgtmpt  47495  smfpimgtxrmptf  47498  smfpimcclem  47521  smfpimcc  47522  smflimmpt  47524  smfsupmpt  47529  smfsupxr  47530  smfinfmpt  47533  smflimsuplem2  47535  smflimsuplem7  47540  smflimsupmpt  47543  smfliminfmpt  47546  cfsetsnfsetf  47795  1arymaptfo  49423  2arymaptfo  49434  setrec2mpt  50475  aacllem  50621