Theorem nfmpt1 5164

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  Ⅎwnfc 2961  {copab 5128   ↦ cmpt 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-opab 5129  df-mpt 5147

This theorem is referenced by:  nffvmpt1  6681  fvmptss  6780  fvmptd3f  6783  mpteqb  6787  fvmptf  6789  ralrnmptw  6860  ralrnmpt  6862  f1ompt  6875  f1mpt  7019  fliftfun  7065  rdgsucmptf  8064  rdgsucmptnf  8065  frsucmpt  8073  frsucmptn  8074  dom2lem  8549  mapxpen  8683  cnfcom3clem  9168  infxpenc2lem2  9446  dfac8clem  9458  acnlem  9474  fin23lem32  9766  axcc3  9860  ac6num  9901  nfcprod1  15264  yonedalem4b  17526  prdsgsum  19101  cayleyhamilton1  21500  neiptopreu  21741  2ndcdisj  22064  ptcnp  22230  cnmpt11  22271  cnmptk2  22294  xkocnv  22422  utopsnneiplem  22856  restmetu  23180  mbfposr  24253  mbfsup  24265  itg1climres  24315  itg2splitlem  24349  itg2split  24350  itg2cnlem1  24362  nfitg1  24374  dvlipcn  24591  lhop2  24612  dvfsumabs  24620  itgparts  24644  itgsubstlem  24645  itgulm2  24997  lgamgulm2  25613  lgseisenlem2  25952  istrkg2ld  26246  cnlnadjlem5  29848  acunirnmpt2  30405  acunirnmpt2f  30406  aciunf1lem  30407  ofpreima  30410  fnpreimac  30416  disjdsct  30438  fpwrelmap  30469  fedgmullem2  31026  locfinreflem  31104  prodindf  31282  nfesum1  31299  esumc  31310  esumrnmpt2  31327  esumsup  31348  esumgect  31349  esum2d  31352  sigapildsys  31421  ldgenpisyslem1  31422  voliune  31488  oms0  31555  rrvadd  31710  ballotlem7  31793  breprexplema  31901  cvmcov  32510  trpredlem1  33066  trpredrec  33077  rdgssun  34662  exrecfnlem  34663  phpreu  34891  matunitlindflem2  34904  poimirlem16  34923  poimirlem19  34926  itg2addnclem  34958  ftc1anclem5  34986  totbndbnd  35082  mzpsubmpt  39360  eq0rabdioph  39393  eqrabdioph  39394  aomclem8  39681  binomcxplemdvbinom  40705  binomcxplemdvsum  40707  binomcxplemnotnn0  40708  refsumcn  41307  refsum2cnlem1  41314  suprnmpt  41450  disjrnmpt2  41469  disjf1o  41472  fompt  41473  disjinfi  41474  choicefi  41483  axccdom  41507  rnmptbd2lem  41540  infnsuprnmpt  41542  rnmptbdlem  41547  rnmptss2  41549  rnmptssbi  41554  supxrleubrnmpt  41699  suprleubrnmpt  41716  infrnmptle  41717  infxrunb3rnmpt  41722  uzub  41725  supminfrnmpt  41739  infxrgelbrnmpt  41750  infrpgernmpt  41761  supminfxrrnmpt  41767  fmuldfeqlem1  41883  fmuldfeq  41884  climneg  41911  climdivf  41913  mullimc  41917  idlimc  41927  sumnnodd  41931  neglimc  41948  addlimc  41949  0ellimcdiv  41950  fnlimfvre  41975  fnlimabslt  41980  climreclmpt  41985  climfveqmpt2  41994  climeldmeqmpt2  41996  climeqmpt  41998  limsupubuz  42014  climinfmpt  42016  limsupubuzmpt  42020  limsupequzmptlem  42029  limsupre2mpt  42031  limsupre3mpt  42035  limsupreuzmpt  42040  liminflelimsuplem  42076  liminfvalxr  42084  liminfvalxrmpt  42087  liminfltlem  42105  liminflbuz2  42116  liminfpnfuz  42117  xlimmnfmpt  42144  xlimpnfmpt  42145  xlimpnfxnegmnf2  42159  cncfmptssg  42173  cncfshift  42177  cncficcgt0  42191  cncfiooicclem1  42196  dvnmul  42248  dvmptfprod  42250  itgsin0pilem1  42255  ibliccsinexp  42256  itgsinexplem1  42259  itgsinexp  42260  iblspltprt  42278  itgsubsticclem  42280  stoweidlem16  42321  stoweidlem18  42323  stoweidlem19  42324  stoweidlem20  42325  stoweidlem22  42327  stoweidlem23  42328  stoweidlem27  42332  stoweidlem31  42336  stoweidlem32  42337  stoweidlem34  42339  stoweidlem35  42340  stoweidlem36  42341  stoweidlem40  42345  stoweidlem41  42346  stoweidlem42  42347  stoweidlem43  42348  stoweidlem44  42349  stoweidlem45  42350  stoweidlem48  42353  stoweidlem51  42356  stoweidlem55  42360  stoweidlem59  42364  stoweidlem60  42365  stoweidlem62  42367  wallispilem5  42374  stirlinglem4  42382  stirlinglem5  42383  stirlinglem8  42386  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  stirlinglem14  42392  stirlinglem15  42393  stirling  42394  fourierdlem16  42428  fourierdlem21  42433  fourierdlem22  42434  fourierdlem53  42464  fourierdlem68  42479  fourierdlem73  42484  fourierdlem80  42491  fourierdlem89  42500  fourierdlem91  42502  fourierdlem93  42504  fourierdlem103  42514  fourierdlem104  42515  fourierdlem112  42523  fourierdlem115  42526  fourierd  42527  fourierclimd  42528  etransclem48  42587  sge00  42678  sge0revalmpt  42680  sge0f1o  42684  sge0fsummpt  42692  sge0gerp  42697  sge0pnffigt  42698  sge0lefi  42700  sge0ltfirp  42702  sge0resplit  42708  sge0iunmptlemfi  42715  sge0iunmpt  42720  sge0xadd  42737  sge0fsummptf  42738  sge0gtfsumgt  42745  sge0reuz  42749  iundjiun  42762  meaiuninc3v  42786  omeiunltfirp  42821  omeiunlempt  42822  hoicvrrex  42858  ovncvrrp  42866  ovnhoilem1  42903  ovnlecvr2  42912  opnvonmbllem1  42934  iunhoiioolem  42977  pimgtmnf  43020  smfpimltmpt  43043  issmfdmpt  43045  smfconst  43046  smfpimltxrmpt  43055  smflimlem2  43068  smflim  43073  smfpimgtmpt  43077  smfpimgtxrmpt  43080  smfpimcclem  43101  smfpimcc  43102  smflimmpt  43104  smfsupmpt  43109  smfsupxr  43110  smfinfmpt  43113  smflimsuplem2  43115  smflimsuplem7  43120  smflimsupmpt  43123  smfliminfmpt  43126  aacllem  44922