Theorem nfmpt1 5191

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

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

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 5155  df-mpt 5174

This theorem is referenced by:  nffvmpt1  6833  fvmptss  6942  fvmptd3f  6945  mpteqb  6949  fvmptf  6951  ralrnmptw  7028  ralrnmpt  7030  f1ompt  7045  fompt  7052  f1mpt  7198  fliftfun  7249  rdgsucmptf  8350  rdgsucmptnf  8351  frsucmpt  8360  frsucmptn  8361  dom2lem  8917  mapxpen  9060  cnfcom3clem  9601  ttrclselem1  9621  ttrclselem2  9622  infxpenc2lem2  9914  dfac8clem  9926  acnlem  9942  fin23lem32  10238  axcc3  10332  ac6num  10373  nfcprod1  15815  yonedalem4b  18182  prdsgsum  19860  cayleyhamilton1  22777  neiptopreu  23018  2ndcdisj  23341  ptcnp  23507  cnmpt11  23548  cnmptk2  23571  xkocnv  23699  utopsnneiplem  24133  restmetu  24456  mbfposr  25551  mbfsup  25563  itg1climres  25613  itg2splitlem  25647  itg2split  25648  itg2cnlem1  25660  nfitg1  25673  dvlipcn  25897  lhop2  25918  dvfsumabs  25927  itgparts  25952  itgsubstlem  25953  itgulm2  26316  lgamgulm2  26944  lgseisenlem2  27285  istrkg2ld  28405  cnlnadjlem5  32015  acunirnmpt2  32603  acunirnmpt2f  32604  aciunf1lem  32605  ofpreima  32608  fnpreimac  32614  disjdsct  32645  fpwrelmap  32676  prodindf  32806  elrgspnsubrunlem2  33188  nsgqusf1olem1  33350  nsgqusf1olem3  33352  elrspunidl  33365  mplvrpmga  33546  fedgmullem2  33597  locfinreflem  33807  nfesum1  34007  esumc  34018  esumrnmpt2  34035  esumsup  34056  esumgect  34057  esum2d  34060  sigapildsys  34129  ldgenpisyslem1  34130  voliune  34196  oms0  34265  rrvadd  34420  ballotlem7  34504  breprexplema  34598  cvmcov  35236  rdgssun  37352  exrecfnlem  37353  phpreu  37584  matunitlindflem2  37597  poimirlem16  37616  poimirlem19  37619  itg2addnclem  37651  ftc1anclem5  37677  totbndbnd  37769  pwsgprod  42517  mzpsubmpt  42716  eq0rabdioph  42749  eqrabdioph  42750  aomclem8  43034  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  refsumcn  45008  refsum2cnlem1  45015  disjrnmpt2  45166  disjf1o  45169  disjinfi  45170  choicefi  45178  axccdom  45200  rnmptbd2lem  45226  infnsuprnmpt  45228  rnmptbdlem  45233  rnmptss2  45235  rnmptssbi  45238  supxrleubrnmpt  45385  suprleubrnmpt  45401  infrnmptle  45402  infxrunb3rnmpt  45407  uzub  45410  supminfrnmpt  45424  infxrgelbrnmpt  45433  infrpgernmpt  45444  supminfxrrnmpt  45450  fmuldfeqlem1  45563  fmuldfeq  45564  climneg  45591  climdivf  45593  mullimc  45597  idlimc  45607  sumnnodd  45611  neglimc  45628  addlimc  45629  0ellimcdiv  45630  fnlimfvre  45655  fnlimabslt  45660  climreclmpt  45665  climfveqmpt2  45674  climeldmeqmpt2  45676  climeqmpt  45678  limsupubuz  45694  climinfmpt  45696  limsupubuzmpt  45700  limsupequzmptlem  45709  limsupre2mpt  45711  limsupre3mpt  45715  limsupreuzmpt  45720  liminflelimsuplem  45756  liminfvalxr  45764  liminfvalxrmpt  45767  liminfltlem  45785  liminflbuz2  45796  liminfpnfuz  45797  xlimmnfmpt  45824  xlimpnfmpt  45825  xlimpnfxnegmnf2  45839  cncfmptssg  45852  cncfshift  45855  cncficcgt0  45869  cncfiooicclem1  45874  dvnmul  45924  dvmptfprod  45926  itgsin0pilem1  45931  ibliccsinexp  45932  itgsinexplem1  45935  itgsinexp  45936  iblspltprt  45954  itgsubsticclem  45956  stoweidlem16  45997  stoweidlem18  45999  stoweidlem19  46000  stoweidlem20  46001  stoweidlem22  46003  stoweidlem23  46004  stoweidlem27  46008  stoweidlem31  46012  stoweidlem32  46013  stoweidlem34  46015  stoweidlem35  46016  stoweidlem36  46017  stoweidlem40  46021  stoweidlem41  46022  stoweidlem42  46023  stoweidlem43  46024  stoweidlem44  46025  stoweidlem45  46026  stoweidlem48  46029  stoweidlem51  46032  stoweidlem55  46036  stoweidlem59  46040  stoweidlem60  46041  stoweidlem62  46043  wallispilem5  46050  stirlinglem4  46058  stirlinglem5  46059  stirlinglem8  46062  stirlinglem11  46065  stirlinglem12  46066  stirlinglem13  46067  stirlinglem14  46068  stirlinglem15  46069  stirling  46070  fourierdlem16  46104  fourierdlem21  46109  fourierdlem22  46110  fourierdlem68  46155  fourierdlem73  46160  fourierdlem80  46167  fourierdlem89  46176  fourierdlem91  46178  fourierdlem93  46180  fourierdlem103  46190  fourierdlem104  46191  fourierdlem112  46199  fourierdlem115  46202  fourierd  46203  fourierclimd  46204  etransclem48  46263  sge00  46357  sge0revalmpt  46359  sge0f1o  46363  sge0fsummpt  46371  sge0gerp  46376  sge0pnffigt  46377  sge0lefi  46379  sge0ltfirp  46381  sge0resplit  46387  sge0iunmptlemfi  46394  sge0iunmpt  46399  sge0xadd  46416  sge0fsummptf  46417  sge0gtfsumgt  46424  sge0reuz  46428  iundjiun  46441  meaiuninc3v  46465  omeiunltfirp  46500  omeiunlempt  46501  hoicvrrex  46537  ovncvrrp  46545  ovnhoilem1  46582  ovnlecvr2  46591  opnvonmbllem1  46613  iunhoiioolem  46656  smfpimltmpt  46727  issmfdmpt  46729  smfconst  46730  smfpimltxrmptf  46739  smflimlem2  46753  smflim  46758  smfpimgtmpt  46762  smfpimgtxrmptf  46765  smfpimcclem  46788  smfpimcc  46789  smflimmpt  46791  smfsupmpt  46796  smfsupxr  46797  smfinfmpt  46800  smflimsuplem2  46802  smflimsuplem7  46807  smflimsupmpt  46810  smfliminfmpt  46813  cfsetsnfsetf  47042  1arymaptfo  48628  2arymaptfo  48639  setrec2mpt  49682  aacllem  49786