Theorem nfmpt1 5206

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Ⅎwnfc 2876  {copab 5169   ↦ cmpt 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-opab 5170  df-mpt 5189

This theorem is referenced by:  nffvmpt1  6869  fvmptss  6980  fvmptd3f  6983  mpteqb  6987  fvmptf  6989  ralrnmptw  7066  ralrnmpt  7068  f1ompt  7083  fompt  7090  f1mpt  7236  fliftfun  7287  rdgsucmptf  8396  rdgsucmptnf  8397  frsucmpt  8406  frsucmptn  8407  dom2lem  8963  mapxpen  9107  cnfcom3clem  9658  ttrclselem1  9678  ttrclselem2  9679  infxpenc2lem2  9973  dfac8clem  9985  acnlem  10001  fin23lem32  10297  axcc3  10391  ac6num  10432  nfcprod1  15874  yonedalem4b  18237  prdsgsum  19911  cayleyhamilton1  22779  neiptopreu  23020  2ndcdisj  23343  ptcnp  23509  cnmpt11  23550  cnmptk2  23573  xkocnv  23701  utopsnneiplem  24135  restmetu  24458  mbfposr  25553  mbfsup  25565  itg1climres  25615  itg2splitlem  25649  itg2split  25650  itg2cnlem1  25662  nfitg1  25675  dvlipcn  25899  lhop2  25920  dvfsumabs  25929  itgparts  25954  itgsubstlem  25955  itgulm2  26318  lgamgulm2  26946  lgseisenlem2  27287  istrkg2ld  28387  cnlnadjlem5  32000  acunirnmpt2  32584  acunirnmpt2f  32585  aciunf1lem  32586  ofpreima  32589  fnpreimac  32595  disjdsct  32626  fpwrelmap  32656  prodindf  32786  elrgspnsubrunlem2  33199  nsgqusf1olem1  33384  nsgqusf1olem3  33386  elrspunidl  33399  fedgmullem2  33626  locfinreflem  33830  nfesum1  34030  esumc  34041  esumrnmpt2  34058  esumsup  34079  esumgect  34080  esum2d  34083  sigapildsys  34152  ldgenpisyslem1  34153  voliune  34219  oms0  34288  rrvadd  34443  ballotlem7  34527  breprexplema  34621  cvmcov  35250  rdgssun  37366  exrecfnlem  37367  phpreu  37598  matunitlindflem2  37611  poimirlem16  37630  poimirlem19  37633  itg2addnclem  37665  ftc1anclem5  37691  totbndbnd  37783  pwsgprod  42532  mzpsubmpt  42731  eq0rabdioph  42764  eqrabdioph  42765  aomclem8  43050  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  refsumcn  45024  refsum2cnlem1  45031  disjrnmpt2  45182  disjf1o  45185  disjinfi  45186  choicefi  45194  axccdom  45216  rnmptbd2lem  45242  infnsuprnmpt  45244  rnmptbdlem  45249  rnmptss2  45251  rnmptssbi  45254  supxrleubrnmpt  45402  suprleubrnmpt  45418  infrnmptle  45419  infxrunb3rnmpt  45424  uzub  45427  supminfrnmpt  45441  infxrgelbrnmpt  45450  infrpgernmpt  45461  supminfxrrnmpt  45467  fmuldfeqlem1  45580  fmuldfeq  45581  climneg  45608  climdivf  45610  mullimc  45614  idlimc  45624  sumnnodd  45628  neglimc  45645  addlimc  45646  0ellimcdiv  45647  fnlimfvre  45672  fnlimabslt  45677  climreclmpt  45682  climfveqmpt2  45691  climeldmeqmpt2  45693  climeqmpt  45695  limsupubuz  45711  climinfmpt  45713  limsupubuzmpt  45717  limsupequzmptlem  45726  limsupre2mpt  45728  limsupre3mpt  45732  limsupreuzmpt  45737  liminflelimsuplem  45773  liminfvalxr  45781  liminfvalxrmpt  45784  liminfltlem  45802  liminflbuz2  45813  liminfpnfuz  45814  xlimmnfmpt  45841  xlimpnfmpt  45842  xlimpnfxnegmnf2  45856  cncfmptssg  45869  cncfshift  45872  cncficcgt0  45886  cncfiooicclem1  45891  dvnmul  45941  dvmptfprod  45943  itgsin0pilem1  45948  ibliccsinexp  45949  itgsinexplem1  45952  itgsinexp  45953  iblspltprt  45971  itgsubsticclem  45973  stoweidlem16  46014  stoweidlem18  46016  stoweidlem19  46017  stoweidlem20  46018  stoweidlem22  46020  stoweidlem23  46021  stoweidlem27  46025  stoweidlem31  46029  stoweidlem32  46030  stoweidlem34  46032  stoweidlem35  46033  stoweidlem36  46034  stoweidlem40  46038  stoweidlem41  46039  stoweidlem42  46040  stoweidlem43  46041  stoweidlem44  46042  stoweidlem45  46043  stoweidlem48  46046  stoweidlem51  46049  stoweidlem55  46053  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  wallispilem5  46067  stirlinglem4  46075  stirlinglem5  46076  stirlinglem8  46079  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  stirling  46087  fourierdlem16  46121  fourierdlem21  46126  fourierdlem22  46127  fourierdlem68  46172  fourierdlem73  46177  fourierdlem80  46184  fourierdlem89  46193  fourierdlem91  46195  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem115  46219  fourierd  46220  fourierclimd  46221  etransclem48  46280  sge00  46374  sge0revalmpt  46376  sge0f1o  46380  sge0fsummpt  46388  sge0gerp  46393  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0resplit  46404  sge0iunmptlemfi  46411  sge0iunmpt  46416  sge0xadd  46433  sge0fsummptf  46434  sge0gtfsumgt  46441  sge0reuz  46445  iundjiun  46458  meaiuninc3v  46482  omeiunltfirp  46517  omeiunlempt  46518  hoicvrrex  46554  ovncvrrp  46562  ovnhoilem1  46599  ovnlecvr2  46608  opnvonmbllem1  46630  iunhoiioolem  46673  smfpimltmpt  46744  issmfdmpt  46746  smfconst  46747  smfpimltxrmptf  46756  smflimlem2  46770  smflim  46775  smfpimgtmpt  46779  smfpimgtxrmptf  46782  smfpimcclem  46805  smfpimcc  46806  smflimmpt  46808  smfsupmpt  46813  smfsupxr  46814  smfinfmpt  46817  smflimsuplem2  46819  smflimsuplem7  46824  smflimsupmpt  46827  smfliminfmpt  46830  cfsetsnfsetf  47059  1arymaptfo  48632  2arymaptfo  48643  setrec2mpt  49686  aacllem  49790