Theorem nfmpt1 5203

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Ⅎwnfc 2907  {copab 5166   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-opab 5167  df-mpt 5186

This theorem is used by:  nffvmpt1  6901  fvmptss  7011  fvmptd3f  7014  mpteqb  7018  fvmptf  7020  ralrnmptw  7099  ralrnmpt  7101  f1ompt  7116  fompt  7123  f1mpt  7269  fliftfun  7324  rdgsucmptf  8443  rdgsucmptnf  8444  frsucmpt  8453  frsucmptn  8454  dom2lem  9026  mapxpen  9169  cnfcom3clem  9713  ttrclselem1  9733  ttrclselem2  9734  infxpenc2lem2  10106  dfac8clem  10118  acnlem  10134  fin23lem32  10429  axcc3  10523  ac6num  10564  nfcprod1  16086  yonedalem4b  18459  prdsgsum  20204  pwsgprod  20568  matunitlindflem2  23004  cayleyhamilton1  23219  neiptopreu  23460  2ndcdisj  23784  ptcnp  23950  cnmpt11  23991  cnmptk2  24014  xkocnv  24142  utopsnneiplem  24575  restmetu  24898  mbfposr  25982  mbfsup  25994  itg1climres  26044  itg2splitlem  26078  itg2split  26079  itg2cnlem1  26091  nfitg1  26103  dvlipcn  26323  lhop2  26344  dvfsumabs  26352  itgparts  26376  itgsubstlem  26377  itgulm2  26745  lgamgulm2  27372  lgseisenlem2  27712  istrkg2ld  28931  cnlnadjlem5  32682  acunirnmpt2  33305  acunirnmpt2f  33306  aciunf1lem  33307  ofpreima  33310  fnpreimac  33315  disjdsct  33347  fpwrelmap  33375  prodindf  33479  suppgsumssiun  33683  elrgspnsubrunlem2  33859  nsgqusf1olem1  34014  nsgqusf1olem3  34016  elrspunidl  34028  deg1prod  34165  mplvrpmga  34227  esplyfval1  34255  fedgmullem2  34312  locfinreflem  34522  nfesum1  34722  esumc  34733  esumrnmpt2  34750  esumsup  34771  esumgect  34772  esum2d  34775  sigapildsys  34845  ldgenpisyslem1  34846  voliune  34912  oms0  34979  rrvadd  35134  ballotlem7  35218  breprexplema  35309  cvmcov  36118  rdgssun  38410  exrecfnlem  38411  phpreu  38636  poimirlem16  38663  poimirlem19  38666  itg2addnclem  38698  ftc1anclem5  38724  totbndbnd  38832  mzpsubmpt  43863  eq0rabdioph  43896  eqrabdioph  43897  aomclem8  44172  binomcxplemdvbinom  45446  binomcxplemdvsum  45448  binomcxplemnotnn0  45449  refsumcn  46155  refsum2cnlem1  46162  disjrnmpt2  46311  disjf1o  46314  disjinfi  46315  choicefi  46322  axccdom  46343  rnmptbd2lem  46368  infnsuprnmpt  46370  rnmptbdlem  46375  rnmptss2  46377  rnmptssbi  46380  supxrleubrnmpt  46524  suprleubrnmpt  46540  infrnmptle  46541  infxrunb3rnmpt  46546  uzub  46549  supminfrnmpt  46563  infxrgelbrnmpt  46572  infrpgernmpt  46583  supminfxrrnmpt  46589  fmuldfeqlem1  46702  fmuldfeq  46703  climneg  46730  climdivf  46732  mullimc  46736  idlimc  46746  sumnnodd  46750  neglimc  46765  addlimc  46766  0ellimcdiv  46767  fnlimfvre  46792  fnlimabslt  46797  climreclmpt  46802  climfveqmpt2  46811  climeldmeqmpt2  46813  climeqmpt  46815  limsupubuz  46831  climinfmpt  46833  limsupubuzmpt  46837  limsupequzmptlem  46846  limsupre2mpt  46848  limsupre3mpt  46852  limsupreuzmpt  46857  liminflelimsuplem  46893  liminfvalxr  46901  liminfvalxrmpt  46904  liminfltlem  46922  liminflbuz2  46933  liminfpnfuz  46934  xlimmnfmpt  46961  xlimpnfmpt  46962  xlimpnfxnegmnf2  46976  cncfmptssg  46989  cncfshift  46992  cncficcgt0  47006  cncfiooicclem1  47011  dvnmul  47061  dvmptfprod  47063  itgsin0pilem1  47068  ibliccsinexp  47069  itgsinexplem1  47072  itgsinexp  47073  iblspltprt  47091  itgsubsticclem  47093  stoweidlem16  47134  stoweidlem18  47136  stoweidlem19  47137  stoweidlem20  47138  stoweidlem22  47140  stoweidlem23  47141  stoweidlem27  47145  stoweidlem31  47149  stoweidlem32  47150  stoweidlem34  47152  stoweidlem35  47153  stoweidlem36  47154  stoweidlem40  47158  stoweidlem41  47159  stoweidlem42  47160  stoweidlem43  47161  stoweidlem44  47162  stoweidlem45  47163  stoweidlem48  47166  stoweidlem51  47169  stoweidlem55  47173  stoweidlem59  47177  stoweidlem60  47178  stoweidlem62  47180  wallispilem5  47187  stirlinglem4  47195  stirlinglem5  47196  stirlinglem8  47199  stirlinglem11  47202  stirlinglem12  47203  stirlinglem13  47204  stirlinglem14  47205  stirlinglem15  47206  stirling  47207  fourierdlem16  47241  fourierdlem21  47246  fourierdlem22  47247  fourierdlem68  47292  fourierdlem73  47297  fourierdlem80  47304  fourierdlem89  47313  fourierdlem91  47315  fourierdlem93  47317  fourierdlem103  47327  fourierdlem104  47328  fourierdlem112  47336  fourierdlem115  47339  fourierd  47340  fourierclimd  47341  etransclem48  47400  sge00  47494  sge0revalmpt  47496  sge0f1o  47500  sge0fsummpt  47508  sge0gerp  47513  sge0pnffigt  47514  sge0lefi  47516  sge0ltfirp  47518  sge0resplit  47524  sge0iunmptlemfi  47531  sge0iunmpt  47536  sge0xadd  47553  sge0fsummptf  47554  sge0gtfsumgt  47561  sge0reuz  47565  iundjiun  47578  meaiuninc3v  47602  omeiunltfirp  47637  omeiunlempt  47638  hoicvrrex  47674  ovncvrrp  47682  ovnhoilem1  47719  ovnlecvr2  47728  opnvonmbllem1  47750  iunhoiioolem  47793  smfpimltmpt  47864  issmfdmpt  47866  smfconst  47867  smfpimltxrmptf  47876  smflimlem2  47890  smflim  47895  smfpimgtmpt  47899  smfpimgtxrmptf  47902  smfpimcclem  47925  smfpimcc  47926  smflimmpt  47928  smfsupmpt  47933  smfsupxr  47934  smfinfmpt  47937  smflimsuplem2  47939  smflimsuplem7  47944  smflimsupmpt  47947  smfliminfmpt  47950  cfsetsnfsetf  48236  1arymaptfo  49863  2arymaptfo  49874  setrec2mpt  50973  aacllem  51122