MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfmpt1 Structured version   Visualization version   GIF version

Theorem nfmpt1 4780
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.
StepHypRef Expression
1 df-mpt 4763 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
2 nfopab1 4752 . 2 𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
31, 2nfcxfr 2791 1 𝑥(𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wcel 2030  wnfc 2780  {copab 4745  cmpt 4762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-opab 4746  df-mpt 4763
This theorem is referenced by:  nffvmpt1  6237  fvmptss  6331  fvmptd3f  6334  mpteqb  6338  fvmptf  6340  ralrnmpt  6408  f1ompt  6422  f1mpt  6558  fliftfun  6602  rdgsucmptf  7569  rdgsucmptnf  7570  frsucmpt  7578  frsucmptn  7579  dom2lem  8037  mapxpen  8167  cnfcom3clem  8640  infxpenc2lem2  8881  dfac8clem  8893  acnlem  8909  fin23lem32  9204  axcc3  9298  ac6num  9339  nfcprod1  14684  yonedalem4b  16963  prdsgsum  18423  cayleyhamilton1  20745  neiptopreu  20985  2ndcdisj  21307  ptcnp  21473  cnmpt11  21514  cnmptk2  21537  xkocnv  21665  utopsnneiplem  22098  restmetu  22422  mbfposr  23464  mbfsup  23476  itg1climres  23526  itg2splitlem  23560  itg2split  23561  itg2cnlem1  23573  nfitg1  23585  dvlipcn  23802  lhop2  23823  dvfsumabs  23831  itgparts  23855  itgsubstlem  23856  itgulm2  24208  lgamgulm2  24807  lgseisenlem2  25146  istrkg2ld  25404  cnlnadjlem5  29058  acunirnmpt2  29588  acunirnmpt2f  29589  aciunf1lem  29590  ofpreima  29593  disjdsct  29608  fpwrelmap  29636  locfinreflem  30035  prodindf  30213  nfesum1  30230  esumc  30241  esumrnmpt2  30258  esumsup  30279  esumgect  30280  esum2d  30283  sigapildsys  30353  ldgenpisyslem1  30354  voliune  30420  oms0  30487  rrvadd  30642  ballotlem7  30725  breprexplema  30836  cvmcov  31371  trpredlem1  31851  trpredrec  31862  phpreu  33523  matunitlindflem2  33536  poimirlem16  33555  poimirlem19  33558  itg2addnclem  33591  ftc1anclem5  33619  totbndbnd  33718  mzpsubmpt  37623  eq0rabdioph  37657  eqrabdioph  37658  aomclem8  37948  binomcxplemdvbinom  38869  binomcxplemdvsum  38871  binomcxplemnotnn0  38872  refsumcn  39503  refsum2cnlem1  39510  suprnmpt  39669  wessf1ornlem  39685  disjrnmpt2  39689  disjf1o  39692  fompt  39693  disjinfi  39694  choicefi  39706  axccdom  39730  rnmptbd2lem  39777  infnsuprnmpt  39779  rnmptbdlem  39784  rnmptss2  39786  rnmptssbi  39791  supxrleubrnmpt  39945  suprleubrnmpt  39962  infrnmptle  39963  infxrunb3rnmpt  39968  uzub  39971  supminfrnmpt  39985  infxrgelbrnmpt  39996  infrpgernmpt  40008  supminfxrrnmpt  40014  fmuldfeqlem1  40132  fmuldfeq  40133  climneg  40160  climdivf  40162  mullimc  40166  idlimc  40176  sumnnodd  40180  neglimc  40197  addlimc  40198  0ellimcdiv  40199  fnlimfvre  40224  fnlimabslt  40229  climreclmpt  40234  climfveqmpt2  40243  climeldmeqmpt2  40245  climeqmpt  40247  limsupubuz  40263  climinfmpt  40265  limsupubuzmpt  40269  limsupequzmptlem  40278  limsupre2mpt  40280  limsupre3mpt  40284  limsupreuzmpt  40289  liminflelimsuplem  40325  liminfvalxr  40333  liminfvalxrmpt  40336  liminfltlem  40354  xlimmnfmpt  40387  xlimpnfmpt  40388  cncfmptssg  40401  cncfshift  40405  cncficcgt0  40419  cncfiooicclem1  40424  dvnmul  40476  dvmptfprod  40478  itgsin0pilem1  40483  ibliccsinexp  40484  itgsinexplem1  40487  itgsinexp  40488  iblspltprt  40507  itgsubsticclem  40509  stoweidlem16  40551  stoweidlem18  40553  stoweidlem19  40554  stoweidlem20  40555  stoweidlem22  40557  stoweidlem23  40558  stoweidlem27  40562  stoweidlem31  40566  stoweidlem32  40567  stoweidlem34  40569  stoweidlem35  40570  stoweidlem36  40571  stoweidlem40  40575  stoweidlem41  40576  stoweidlem42  40577  stoweidlem43  40578  stoweidlem44  40579  stoweidlem45  40580  stoweidlem48  40583  stoweidlem51  40586  stoweidlem55  40590  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  wallispilem5  40604  stirlinglem4  40612  stirlinglem5  40613  stirlinglem8  40616  stirlinglem11  40619  stirlinglem12  40620  stirlinglem13  40621  stirlinglem14  40622  stirlinglem15  40623  stirling  40624  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem53  40694  fourierdlem68  40709  fourierdlem73  40714  fourierdlem80  40721  fourierdlem89  40730  fourierdlem91  40732  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem115  40756  fourierd  40757  fourierclimd  40758  etransclem48  40817  sge00  40911  sge0revalmpt  40913  sge0f1o  40917  sge0fsummpt  40925  sge0gerp  40930  sge0pnffigt  40931  sge0lefi  40933  sge0ltfirp  40935  sge0resplit  40941  sge0iunmptlemfi  40948  sge0iunmpt  40953  sge0xadd  40970  sge0fsummptf  40971  sge0gtfsumgt  40978  sge0reuz  40982  iundjiun  40995  meaiuninc3v  41019  omeiunltfirp  41054  omeiunlempt  41055  hoicvrrex  41091  ovncvrrp  41099  ovnhoilem1  41136  ovnlecvr2  41145  opnvonmbllem1  41167  iunhoiioolem  41210  pimgtmnf  41253  smfpimltmpt  41276  issmfdmpt  41278  smfconst  41279  smfpimltxrmpt  41288  smflimlem2  41301  smflim  41306  smfpimgtmpt  41310  smfpimgtxrmpt  41313  smfpimcclem  41334  smfpimcc  41335  smflimmpt  41337  smfsupmpt  41342  smfsupxr  41343  smfinfmpt  41346  smflimsuplem2  41348  smflimsuplem7  41353  smflimsupmpt  41356  smfliminfmpt  41359  aacllem  42875
  Copyright terms: Public domain W3C validator