Theorem nfmpt1 5184

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Ⅎwnfc 2883  {copab 5147   ↦ cmpt 5166

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-opab 5148  df-mpt 5167

This theorem is referenced by:  nffvmpt1  6851  fvmptss  6960  fvmptd3f  6963  mpteqb  6967  fvmptf  6969  ralrnmptw  7046  ralrnmpt  7048  f1ompt  7063  fompt  7070  f1mpt  7216  fliftfun  7267  rdgsucmptf  8367  rdgsucmptnf  8368  frsucmpt  8377  frsucmptn  8378  dom2lem  8939  mapxpen  9081  cnfcom3clem  9626  ttrclselem1  9646  ttrclselem2  9647  infxpenc2lem2  9942  dfac8clem  9954  acnlem  9970  fin23lem32  10266  axcc3  10360  ac6num  10401  nfcprod1  15873  yonedalem4b  18242  prdsgsum  19956  pwsgprod  20309  cayleyhamilton1  22857  neiptopreu  23098  2ndcdisj  23421  ptcnp  23587  cnmpt11  23628  cnmptk2  23651  xkocnv  23779  utopsnneiplem  24212  restmetu  24535  mbfposr  25619  mbfsup  25631  itg1climres  25681  itg2splitlem  25715  itg2split  25716  itg2cnlem1  25728  nfitg1  25741  dvlipcn  25961  lhop2  25982  dvfsumabs  25990  itgparts  26014  itgsubstlem  26015  itgulm2  26374  lgamgulm2  26999  lgseisenlem2  27339  istrkg2ld  28528  cnlnadjlem5  32142  acunirnmpt2  32733  acunirnmpt2f  32734  aciunf1lem  32735  ofpreima  32738  fnpreimac  32743  disjdsct  32776  fpwrelmap  32806  prodindf  32922  suppgsumssiun  33133  elrgspnsubrunlem2  33309  nsgqusf1olem1  33473  nsgqusf1olem3  33475  elrspunidl  33488  deg1prod  33643  mplvrpmga  33689  esplyfval1  33717  fedgmullem2  33774  locfinreflem  33984  nfesum1  34184  esumc  34195  esumrnmpt2  34212  esumsup  34233  esumgect  34234  esum2d  34237  sigapildsys  34306  ldgenpisyslem1  34307  voliune  34373  oms0  34441  rrvadd  34596  ballotlem7  34680  breprexplema  34774  cvmcov  35445  rdgssun  37694  exrecfnlem  37695  phpreu  37925  matunitlindflem2  37938  poimirlem16  37957  poimirlem19  37960  itg2addnclem  37992  ftc1anclem5  38018  totbndbnd  38110  mzpsubmpt  43175  eq0rabdioph  43208  eqrabdioph  43209  aomclem8  43489  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  refsumcn  45461  refsum2cnlem1  45468  disjrnmpt2  45618  disjf1o  45621  disjinfi  45622  choicefi  45629  axccdom  45651  rnmptbd2lem  45677  infnsuprnmpt  45679  rnmptbdlem  45684  rnmptss2  45686  rnmptssbi  45689  supxrleubrnmpt  45834  suprleubrnmpt  45850  infrnmptle  45851  infxrunb3rnmpt  45856  uzub  45859  supminfrnmpt  45873  infxrgelbrnmpt  45882  infrpgernmpt  45893  supminfxrrnmpt  45899  fmuldfeqlem1  46012  fmuldfeq  46013  climneg  46040  climdivf  46042  mullimc  46046  idlimc  46056  sumnnodd  46060  neglimc  46075  addlimc  46076  0ellimcdiv  46077  fnlimfvre  46102  fnlimabslt  46107  climreclmpt  46112  climfveqmpt2  46121  climeldmeqmpt2  46123  climeqmpt  46125  limsupubuz  46141  climinfmpt  46143  limsupubuzmpt  46147  limsupequzmptlem  46156  limsupre2mpt  46158  limsupre3mpt  46162  limsupreuzmpt  46167  liminflelimsuplem  46203  liminfvalxr  46211  liminfvalxrmpt  46214  liminfltlem  46232  liminflbuz2  46243  liminfpnfuz  46244  xlimmnfmpt  46271  xlimpnfmpt  46272  xlimpnfxnegmnf2  46286  cncfmptssg  46299  cncfshift  46302  cncficcgt0  46316  cncfiooicclem1  46321  dvnmul  46371  dvmptfprod  46373  itgsin0pilem1  46378  ibliccsinexp  46379  itgsinexplem1  46382  itgsinexp  46383  iblspltprt  46401  itgsubsticclem  46403  stoweidlem16  46444  stoweidlem18  46446  stoweidlem19  46447  stoweidlem20  46448  stoweidlem22  46450  stoweidlem23  46451  stoweidlem27  46455  stoweidlem31  46459  stoweidlem32  46460  stoweidlem34  46462  stoweidlem35  46463  stoweidlem36  46464  stoweidlem40  46468  stoweidlem41  46469  stoweidlem42  46470  stoweidlem43  46471  stoweidlem44  46472  stoweidlem45  46473  stoweidlem48  46476  stoweidlem51  46479  stoweidlem55  46483  stoweidlem59  46487  stoweidlem60  46488  stoweidlem62  46490  wallispilem5  46497  stirlinglem4  46505  stirlinglem5  46506  stirlinglem8  46509  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  stirling  46517  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem68  46602  fourierdlem73  46607  fourierdlem80  46614  fourierdlem89  46623  fourierdlem91  46625  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  fourierdlem112  46646  fourierdlem115  46649  fourierd  46650  fourierclimd  46651  etransclem48  46710  sge00  46804  sge0revalmpt  46806  sge0f1o  46810  sge0fsummpt  46818  sge0gerp  46823  sge0pnffigt  46824  sge0lefi  46826  sge0ltfirp  46828  sge0resplit  46834  sge0iunmptlemfi  46841  sge0iunmpt  46846  sge0xadd  46863  sge0fsummptf  46864  sge0gtfsumgt  46871  sge0reuz  46875  iundjiun  46888  meaiuninc3v  46912  omeiunltfirp  46947  omeiunlempt  46948  hoicvrrex  46984  ovncvrrp  46992  ovnhoilem1  47029  ovnlecvr2  47038  opnvonmbllem1  47060  iunhoiioolem  47103  smfpimltmpt  47174  issmfdmpt  47176  smfconst  47177  smfpimltxrmptf  47186  smflimlem2  47200  smflim  47205  smfpimgtmpt  47209  smfpimgtxrmptf  47212  smfpimcclem  47235  smfpimcc  47236  smflimmpt  47238  smfsupmpt  47243  smfsupxr  47244  smfinfmpt  47247  smflimsuplem2  47249  smflimsuplem7  47254  smflimsupmpt  47257  smfliminfmpt  47260  cfsetsnfsetf  47506  1arymaptfo  49119  2arymaptfo  49130  setrec2mpt  50172  aacllem  50276