Theorem nfmpt1 5199

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

Syntax hints:   ∧ wa 399   = wceq 1560   ∈ wcel 2142  Ⅎwnfc 2909  {copab 5162   ↦ cmpt 5181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-opab 5163  df-mpt 5182

This theorem is referenced by:  nffvmpt1  6878  fvmptss  6988  fvmptd3f  6991  mpteqb  6995  fvmptf  6997  ralrnmptw  7075  ralrnmpt  7077  f1ompt  7092  fompt  7099  f1mpt  7245  fliftfun  7296  rdgsucmptf  8399  rdgsucmptnf  8400  frsucmpt  8409  frsucmptn  8410  dom2lem  8973  mapxpen  9115  cnfcom3clem  9660  ttrclselem1  9680  ttrclselem2  9681  infxpenc2lem2  9976  dfac8clem  9988  acnlem  10004  fin23lem32  10301  axcc3  10395  ac6num  10436  nfcprod1  15938  yonedalem4b  18308  prdsgsum  20021  pwsgprod  20374  cayleyhamilton1  22949  neiptopreu  23190  2ndcdisj  23513  ptcnp  23679  cnmpt11  23720  cnmptk2  23743  xkocnv  23871  utopsnneiplem  24304  restmetu  24627  mbfposr  25711  mbfsup  25723  itg1climres  25773  itg2splitlem  25807  itg2split  25808  itg2cnlem1  25820  nfitg1  25833  dvlipcn  26053  lhop2  26074  dvfsumabs  26082  itgparts  26106  itgsubstlem  26107  itgulm2  26469  lgamgulm2  27097  lgseisenlem2  27437  istrkg2ld  28626  cnlnadjlem5  32271  acunirnmpt2  32859  acunirnmpt2f  32860  aciunf1lem  32861  ofpreima  32864  fnpreimac  32869  disjdsct  32902  fpwrelmap  32932  prodindf  33037  suppgsumssiun  33249  elrgspnsubrunlem2  33426  nsgqusf1olem1  33596  nsgqusf1olem3  33598  elrspunidl  33611  deg1prod  33776  mplvrpmga  33839  esplyfval1  33867  fedgmullem2  33924  locfinreflem  34134  nfesum1  34334  esumc  34345  esumrnmpt2  34362  esumsup  34383  esumgect  34384  esum2d  34387  sigapildsys  34456  ldgenpisyslem1  34457  voliune  34523  oms0  34591  rrvadd  34746  ballotlem7  34830  breprexplema  34921  cvmcov  35610  rdgssun  37869  exrecfnlem  37870  phpreu  38100  matunitlindflem2  38113  poimirlem16  38132  poimirlem19  38135  itg2addnclem  38167  ftc1anclem5  38193  totbndbnd  38285  mzpsubmpt  43321  eq0rabdioph  43354  eqrabdioph  43355  aomclem8  43635  binomcxplemdvbinom  44926  binomcxplemdvsum  44928  binomcxplemnotnn0  44929  refsumcn  45607  refsum2cnlem1  45614  disjrnmpt2  45763  disjf1o  45766  disjinfi  45767  choicefi  45774  axccdom  45795  rnmptbd2lem  45820  infnsuprnmpt  45822  rnmptbdlem  45827  rnmptss2  45829  rnmptssbi  45832  supxrleubrnmpt  45977  suprleubrnmpt  45993  infrnmptle  45994  infxrunb3rnmpt  45999  uzub  46002  supminfrnmpt  46016  infxrgelbrnmpt  46025  infrpgernmpt  46036  supminfxrrnmpt  46042  fmuldfeqlem1  46155  fmuldfeq  46156  climneg  46183  climdivf  46185  mullimc  46189  idlimc  46199  sumnnodd  46203  neglimc  46218  addlimc  46219  0ellimcdiv  46220  fnlimfvre  46245  fnlimabslt  46250  climreclmpt  46255  climfveqmpt2  46264  climeldmeqmpt2  46266  climeqmpt  46268  limsupubuz  46284  climinfmpt  46286  limsupubuzmpt  46290  limsupequzmptlem  46299  limsupre2mpt  46301  limsupre3mpt  46305  limsupreuzmpt  46310  liminflelimsuplem  46346  liminfvalxr  46354  liminfvalxrmpt  46357  liminfltlem  46375  liminflbuz2  46386  liminfpnfuz  46387  xlimmnfmpt  46414  xlimpnfmpt  46415  xlimpnfxnegmnf2  46429  cncfmptssg  46442  cncfshift  46445  cncficcgt0  46459  cncfiooicclem1  46464  dvnmul  46514  dvmptfprod  46516  itgsin0pilem1  46521  ibliccsinexp  46522  itgsinexplem1  46525  itgsinexp  46526  iblspltprt  46544  itgsubsticclem  46546  stoweidlem16  46587  stoweidlem18  46589  stoweidlem19  46590  stoweidlem20  46591  stoweidlem22  46593  stoweidlem23  46594  stoweidlem27  46598  stoweidlem31  46602  stoweidlem32  46603  stoweidlem34  46605  stoweidlem35  46606  stoweidlem36  46607  stoweidlem40  46611  stoweidlem41  46612  stoweidlem42  46613  stoweidlem43  46614  stoweidlem44  46615  stoweidlem45  46616  stoweidlem48  46619  stoweidlem51  46622  stoweidlem55  46626  stoweidlem59  46630  stoweidlem60  46631  stoweidlem62  46633  wallispilem5  46640  stirlinglem4  46648  stirlinglem5  46649  stirlinglem8  46652  stirlinglem11  46655  stirlinglem12  46656  stirlinglem13  46657  stirlinglem14  46658  stirlinglem15  46659  stirling  46660  fourierdlem16  46694  fourierdlem21  46699  fourierdlem22  46700  fourierdlem68  46745  fourierdlem73  46750  fourierdlem80  46757  fourierdlem89  46766  fourierdlem91  46768  fourierdlem93  46770  fourierdlem103  46780  fourierdlem104  46781  fourierdlem112  46789  fourierdlem115  46792  fourierd  46793  fourierclimd  46794  etransclem48  46853  sge00  46947  sge0revalmpt  46949  sge0f1o  46953  sge0fsummpt  46961  sge0gerp  46966  sge0pnffigt  46967  sge0lefi  46969  sge0ltfirp  46971  sge0resplit  46977  sge0iunmptlemfi  46984  sge0iunmpt  46989  sge0xadd  47006  sge0fsummptf  47007  sge0gtfsumgt  47014  sge0reuz  47018  iundjiun  47031  meaiuninc3v  47055  omeiunltfirp  47090  omeiunlempt  47091  hoicvrrex  47127  ovncvrrp  47135  ovnhoilem1  47172  ovnlecvr2  47181  opnvonmbllem1  47203  iunhoiioolem  47246  smfpimltmpt  47317  issmfdmpt  47319  smfconst  47320  smfpimltxrmptf  47329  smflimlem2  47343  smflim  47348  smfpimgtmpt  47352  smfpimgtxrmptf  47355  smfpimcclem  47378  smfpimcc  47379  smflimmpt  47381  smfsupmpt  47386  smfsupxr  47387  smfinfmpt  47390  smflimsuplem2  47392  smflimsuplem7  47397  smflimsupmpt  47400  smfliminfmpt  47403  cfsetsnfsetf  47649  1arymaptfo  49262  2arymaptfo  49273  setrec2mpt  50315  aacllem  50419