Theorem nfmpt1 5174

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

Syntax hints:   ∧ wa 397   = wceq 1548   ∈ wcel 2121  Ⅎwnfc 2888  {copab 5137   ↦ cmpt 5156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-nf 1792  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-opab 5138  df-mpt 5157

This theorem is referenced by:  nffvmpt1  6842  fvmptss  6952  fvmptd3f  6955  mpteqb  6959  fvmptf  6961  ralrnmptw  7039  ralrnmpt  7041  f1ompt  7056  fompt  7063  f1mpt  7209  fliftfun  7260  rdgsucmptf  8361  rdgsucmptnf  8362  frsucmpt  8371  frsucmptn  8372  dom2lem  8933  mapxpen  9075  cnfcom3clem  9621  ttrclselem1  9641  ttrclselem2  9642  infxpenc2lem2  9937  dfac8clem  9949  acnlem  9965  fin23lem32  10261  axcc3  10355  ac6num  10396  nfcprod1  15868  yonedalem4b  18237  prdsgsum  19951  pwsgprod  20304  cayleyhamilton1  22879  neiptopreu  23120  2ndcdisj  23443  ptcnp  23609  cnmpt11  23650  cnmptk2  23673  xkocnv  23801  utopsnneiplem  24234  restmetu  24557  mbfposr  25641  mbfsup  25653  itg1climres  25703  itg2splitlem  25737  itg2split  25738  itg2cnlem1  25750  nfitg1  25763  dvlipcn  25983  lhop2  26004  dvfsumabs  26012  itgparts  26036  itgsubstlem  26037  itgulm2  26396  lgamgulm2  27021  lgseisenlem2  27361  istrkg2ld  28550  cnlnadjlem5  32164  acunirnmpt2  32756  acunirnmpt2f  32757  aciunf1lem  32758  ofpreima  32761  fnpreimac  32766  disjdsct  32799  fpwrelmap  32829  prodindf  32945  suppgsumssiun  33157  elrgspnsubrunlem2  33333  nsgqusf1olem1  33500  nsgqusf1olem3  33502  elrspunidl  33515  deg1prod  33678  mplvrpmga  33741  esplyfval1  33769  fedgmullem2  33826  locfinreflem  34036  nfesum1  34236  esumc  34247  esumrnmpt2  34264  esumsup  34285  esumgect  34286  esum2d  34289  sigapildsys  34358  ldgenpisyslem1  34359  voliune  34425  oms0  34493  rrvadd  34648  ballotlem7  34732  breprexplema  34826  cvmcov  35506  rdgssun  37755  exrecfnlem  37756  phpreu  37986  matunitlindflem2  37999  poimirlem16  38018  poimirlem19  38021  itg2addnclem  38053  ftc1anclem5  38079  totbndbnd  38171  mzpsubmpt  43207  eq0rabdioph  43240  eqrabdioph  43241  aomclem8  43521  binomcxplemdvbinom  44812  binomcxplemdvsum  44814  binomcxplemnotnn0  44815  refsumcn  45493  refsum2cnlem1  45500  disjrnmpt2  45649  disjf1o  45652  disjinfi  45653  choicefi  45660  axccdom  45681  rnmptbd2lem  45706  infnsuprnmpt  45708  rnmptbdlem  45713  rnmptss2  45715  rnmptssbi  45718  supxrleubrnmpt  45863  suprleubrnmpt  45879  infrnmptle  45880  infxrunb3rnmpt  45885  uzub  45888  supminfrnmpt  45902  infxrgelbrnmpt  45911  infrpgernmpt  45922  supminfxrrnmpt  45928  fmuldfeqlem1  46041  fmuldfeq  46042  climneg  46069  climdivf  46071  mullimc  46075  idlimc  46085  sumnnodd  46089  neglimc  46104  addlimc  46105  0ellimcdiv  46106  fnlimfvre  46131  fnlimabslt  46136  climreclmpt  46141  climfveqmpt2  46150  climeldmeqmpt2  46152  climeqmpt  46154  limsupubuz  46170  climinfmpt  46172  limsupubuzmpt  46176  limsupequzmptlem  46185  limsupre2mpt  46187  limsupre3mpt  46191  limsupreuzmpt  46196  liminflelimsuplem  46232  liminfvalxr  46240  liminfvalxrmpt  46243  liminfltlem  46261  liminflbuz2  46272  liminfpnfuz  46273  xlimmnfmpt  46300  xlimpnfmpt  46301  xlimpnfxnegmnf2  46315  cncfmptssg  46328  cncfshift  46331  cncficcgt0  46345  cncfiooicclem1  46350  dvnmul  46400  dvmptfprod  46402  itgsin0pilem1  46407  ibliccsinexp  46408  itgsinexplem1  46411  itgsinexp  46412  iblspltprt  46430  itgsubsticclem  46432  stoweidlem16  46473  stoweidlem18  46475  stoweidlem19  46476  stoweidlem20  46477  stoweidlem22  46479  stoweidlem23  46480  stoweidlem27  46484  stoweidlem31  46488  stoweidlem32  46489  stoweidlem34  46491  stoweidlem35  46492  stoweidlem36  46493  stoweidlem40  46497  stoweidlem41  46498  stoweidlem42  46499  stoweidlem43  46500  stoweidlem44  46501  stoweidlem45  46502  stoweidlem48  46505  stoweidlem51  46508  stoweidlem55  46512  stoweidlem59  46516  stoweidlem60  46517  stoweidlem62  46519  wallispilem5  46526  stirlinglem4  46534  stirlinglem5  46535  stirlinglem8  46538  stirlinglem11  46541  stirlinglem12  46542  stirlinglem13  46543  stirlinglem14  46544  stirlinglem15  46545  stirling  46546  fourierdlem16  46580  fourierdlem21  46585  fourierdlem22  46586  fourierdlem68  46631  fourierdlem73  46636  fourierdlem80  46643  fourierdlem89  46652  fourierdlem91  46654  fourierdlem93  46656  fourierdlem103  46666  fourierdlem104  46667  fourierdlem112  46675  fourierdlem115  46678  fourierd  46679  fourierclimd  46680  etransclem48  46739  sge00  46833  sge0revalmpt  46835  sge0f1o  46839  sge0fsummpt  46847  sge0gerp  46852  sge0pnffigt  46853  sge0lefi  46855  sge0ltfirp  46857  sge0resplit  46863  sge0iunmptlemfi  46870  sge0iunmpt  46875  sge0xadd  46892  sge0fsummptf  46893  sge0gtfsumgt  46900  sge0reuz  46904  iundjiun  46917  meaiuninc3v  46941  omeiunltfirp  46976  omeiunlempt  46977  hoicvrrex  47013  ovncvrrp  47021  ovnhoilem1  47058  ovnlecvr2  47067  opnvonmbllem1  47089  iunhoiioolem  47132  smfpimltmpt  47203  issmfdmpt  47205  smfconst  47206  smfpimltxrmptf  47215  smflimlem2  47229  smflim  47234  smfpimgtmpt  47238  smfpimgtxrmptf  47241  smfpimcclem  47264  smfpimcc  47265  smflimmpt  47267  smfsupmpt  47272  smfsupxr  47273  smfinfmpt  47276  smflimsuplem2  47278  smflimsuplem7  47283  smflimsupmpt  47286  smfliminfmpt  47289  cfsetsnfsetf  47535  1arymaptfo  49148  2arymaptfo  49159  setrec2mpt  50201  aacllem  50305