Theorem nfmpt1 5249

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Ⅎwnfc 2882  {copab 5203   ↦ cmpt 5224

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-opab 5204  df-mpt 5225

This theorem is referenced by:  nffvmpt1  6889  fvmptss  6996  fvmptd3f  6999  mpteqb  7003  fvmptf  7005  ralrnmptw  7080  ralrnmpt  7082  f1ompt  7095  f1mpt  7244  fliftfun  7293  rdgsucmptf  8410  rdgsucmptnf  8411  frsucmpt  8420  frsucmptn  8421  dom2lem  8971  mapxpen  9126  cnfcom3clem  9682  ttrclselem1  9702  ttrclselem2  9703  infxpenc2lem2  9997  dfac8clem  10009  acnlem  10025  fin23lem32  10321  axcc3  10415  ac6num  10456  nfcprod1  15836  yonedalem4b  18211  prdsgsum  19808  cayleyhamilton1  22323  neiptopreu  22566  2ndcdisj  22889  ptcnp  23055  cnmpt11  23096  cnmptk2  23119  xkocnv  23247  utopsnneiplem  23681  restmetu  24008  mbfposr  25098  mbfsup  25110  itg1climres  25161  itg2splitlem  25195  itg2split  25196  itg2cnlem1  25208  nfitg1  25220  dvlipcn  25440  lhop2  25461  dvfsumabs  25469  itgparts  25493  itgsubstlem  25494  itgulm2  25850  lgamgulm2  26467  lgseisenlem2  26806  istrkg2ld  27576  cnlnadjlem5  31187  acunirnmpt2  31754  acunirnmpt2f  31755  aciunf1lem  31756  ofpreima  31759  fnpreimac  31765  disjdsct  31795  fpwrelmap  31829  nsgqusf1olem1  32380  nsgqusf1olem3  32382  elrspunidl  32397  fedgmullem2  32553  locfinreflem  32651  prodindf  32852  nfesum1  32869  esumc  32880  esumrnmpt2  32897  esumsup  32918  esumgect  32919  esum2d  32922  sigapildsys  32991  ldgenpisyslem1  32992  voliune  33058  oms0  33127  rrvadd  33282  ballotlem7  33365  breprexplema  33473  cvmcov  34085  rdgssun  36063  exrecfnlem  36064  phpreu  36276  matunitlindflem2  36289  poimirlem16  36308  poimirlem19  36311  itg2addnclem  36343  ftc1anclem5  36369  totbndbnd  36462  pwsgprod  40918  mzpsubmpt  41252  eq0rabdioph  41285  eqrabdioph  41286  aomclem8  41574  binomcxplemdvbinom  42883  binomcxplemdvsum  42885  binomcxplemnotnn0  42886  refsumcn  43485  refsum2cnlem1  43492  disjrnmpt2  43657  disjf1o  43660  fompt  43661  disjinfi  43662  choicefi  43670  axccdom  43692  rnmptbd2lem  43725  infnsuprnmpt  43727  rnmptbdlem  43732  rnmptss2  43734  rnmptssbi  43738  supxrleubrnmpt  43889  suprleubrnmpt  43905  infrnmptle  43906  infxrunb3rnmpt  43911  uzub  43914  supminfrnmpt  43928  infxrgelbrnmpt  43937  infrpgernmpt  43948  supminfxrrnmpt  43954  fmuldfeqlem1  44071  fmuldfeq  44072  climneg  44099  climdivf  44101  mullimc  44105  idlimc  44115  sumnnodd  44119  neglimc  44136  addlimc  44137  0ellimcdiv  44138  fnlimfvre  44163  fnlimabslt  44168  climreclmpt  44173  climfveqmpt2  44182  climeldmeqmpt2  44184  climeqmpt  44186  limsupubuz  44202  climinfmpt  44204  limsupubuzmpt  44208  limsupequzmptlem  44217  limsupre2mpt  44219  limsupre3mpt  44223  limsupreuzmpt  44228  liminflelimsuplem  44264  liminfvalxr  44272  liminfvalxrmpt  44275  liminfltlem  44293  liminflbuz2  44304  liminfpnfuz  44305  xlimmnfmpt  44332  xlimpnfmpt  44333  xlimpnfxnegmnf2  44347  cncfmptssg  44360  cncfshift  44363  cncficcgt0  44377  cncfiooicclem1  44382  dvnmul  44432  dvmptfprod  44434  itgsin0pilem1  44439  ibliccsinexp  44440  itgsinexplem1  44443  itgsinexp  44444  iblspltprt  44462  itgsubsticclem  44464  stoweidlem16  44505  stoweidlem18  44507  stoweidlem19  44508  stoweidlem20  44509  stoweidlem22  44511  stoweidlem23  44512  stoweidlem27  44516  stoweidlem31  44520  stoweidlem32  44521  stoweidlem34  44523  stoweidlem35  44524  stoweidlem36  44525  stoweidlem40  44529  stoweidlem41  44530  stoweidlem42  44531  stoweidlem43  44532  stoweidlem44  44533  stoweidlem45  44534  stoweidlem48  44537  stoweidlem51  44540  stoweidlem55  44544  stoweidlem59  44548  stoweidlem60  44549  stoweidlem62  44551  wallispilem5  44558  stirlinglem4  44566  stirlinglem5  44567  stirlinglem8  44570  stirlinglem11  44573  stirlinglem12  44574  stirlinglem13  44575  stirlinglem14  44576  stirlinglem15  44577  stirling  44578  fourierdlem16  44612  fourierdlem21  44617  fourierdlem22  44618  fourierdlem68  44663  fourierdlem73  44668  fourierdlem80  44675  fourierdlem89  44684  fourierdlem91  44686  fourierdlem93  44688  fourierdlem103  44698  fourierdlem104  44699  fourierdlem112  44707  fourierdlem115  44710  fourierd  44711  fourierclimd  44712  etransclem48  44771  sge00  44865  sge0revalmpt  44867  sge0f1o  44871  sge0fsummpt  44879  sge0gerp  44884  sge0pnffigt  44885  sge0lefi  44887  sge0ltfirp  44889  sge0resplit  44895  sge0iunmptlemfi  44902  sge0iunmpt  44907  sge0xadd  44924  sge0fsummptf  44925  sge0gtfsumgt  44932  sge0reuz  44936  iundjiun  44949  meaiuninc3v  44973  omeiunltfirp  45008  omeiunlempt  45009  hoicvrrex  45045  ovncvrrp  45053  ovnhoilem1  45090  ovnlecvr2  45099  opnvonmbllem1  45121  iunhoiioolem  45164  smfpimltmpt  45235  issmfdmpt  45237  smfconst  45238  smfpimltxrmptf  45247  smflimlem2  45261  smflim  45266  smfpimgtmpt  45270  smfpimgtxrmptf  45273  smfpimcclem  45296  smfpimcc  45297  smflimmpt  45299  smfsupmpt  45304  smfsupxr  45305  smfinfmpt  45308  smflimsuplem2  45310  smflimsuplem7  45315  smflimsupmpt  45318  smfliminfmpt  45321  cfsetsnfsetf  45540  1arymaptfo  46977  2arymaptfo  46988  setrec2mpt  47390  aacllem  47496