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

Theorem nfmpt1 4906
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 4889 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
2 nfopab1 4878 . 2 𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
31, 2nfcxfr 2905 1 𝑥(𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1652  wcel 2155  wnfc 2894  {copab 4871  cmpt 4888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-opab 4872  df-mpt 4889
This theorem is referenced by:  nffvmpt1  6386  fvmptss  6481  fvmptd3f  6484  mpteqb  6488  fvmptf  6490  ralrnmpt  6558  f1ompt  6571  f1mpt  6710  fliftfun  6754  rdgsucmptf  7728  rdgsucmptnf  7729  frsucmpt  7737  frsucmptn  7738  dom2lem  8200  mapxpen  8333  cnfcom3clem  8817  infxpenc2lem2  9094  dfac8clem  9106  acnlem  9122  fin23lem32  9419  axcc3  9513  ac6num  9554  nfcprod1  14925  yonedalem4b  17184  prdsgsum  18643  cayleyhamilton1  20976  neiptopreu  21217  2ndcdisj  21539  ptcnp  21705  cnmpt11  21746  cnmptk2  21769  xkocnv  21897  utopsnneiplem  22330  restmetu  22654  mbfposr  23710  mbfsup  23722  itg1climres  23772  itg2splitlem  23806  itg2split  23807  itg2cnlem1  23819  nfitg1  23831  dvlipcn  24048  lhop2  24069  dvfsumabs  24077  itgparts  24101  itgsubstlem  24102  itgulm2  24454  lgamgulm2  25053  lgseisenlem2  25392  istrkg2ld  25650  cnlnadjlem5  29321  acunirnmpt2  29845  acunirnmpt2f  29846  aciunf1lem  29847  ofpreima  29850  disjdsct  29864  fpwrelmap  29892  locfinreflem  30289  prodindf  30467  nfesum1  30484  esumc  30495  esumrnmpt2  30512  esumsup  30533  esumgect  30534  esum2d  30537  sigapildsys  30607  ldgenpisyslem1  30608  voliune  30674  oms0  30741  rrvadd  30897  ballotlem7  30980  breprexplema  31091  cvmcov  31625  trpredlem1  32102  trpredrec  32113  phpreu  33749  matunitlindflem2  33762  poimirlem16  33781  poimirlem19  33784  itg2addnclem  33816  ftc1anclem5  33844  totbndbnd  33942  mzpsubmpt  37916  eq0rabdioph  37950  eqrabdioph  37951  aomclem8  38240  binomcxplemdvbinom  39158  binomcxplemdvsum  39160  binomcxplemnotnn0  39161  refsumcn  39773  refsum2cnlem1  39780  suprnmpt  39934  wessf1ornlem  39950  disjrnmpt2  39954  disjf1o  39957  fompt  39958  disjinfi  39959  choicefi  39969  axccdom  39993  rnmptbd2lem  40036  infnsuprnmpt  40038  rnmptbdlem  40043  rnmptss2  40045  rnmptssbi  40050  supxrleubrnmpt  40201  suprleubrnmpt  40218  infrnmptle  40219  infxrunb3rnmpt  40224  uzub  40227  supminfrnmpt  40241  infxrgelbrnmpt  40252  infrpgernmpt  40264  supminfxrrnmpt  40270  fmuldfeqlem1  40384  fmuldfeq  40385  climneg  40412  climdivf  40414  mullimc  40418  idlimc  40428  sumnnodd  40432  neglimc  40449  addlimc  40450  0ellimcdiv  40451  fnlimfvre  40476  fnlimabslt  40481  climreclmpt  40486  climfveqmpt2  40495  climeldmeqmpt2  40497  climeqmpt  40499  limsupubuz  40515  climinfmpt  40517  limsupubuzmpt  40521  limsupequzmptlem  40530  limsupre2mpt  40532  limsupre3mpt  40536  limsupreuzmpt  40541  liminflelimsuplem  40577  liminfvalxr  40585  liminfvalxrmpt  40588  liminfltlem  40606  xlimmnfmpt  40639  xlimpnfmpt  40640  cncfmptssg  40653  cncfshift  40657  cncficcgt0  40671  cncfiooicclem1  40676  dvnmul  40728  dvmptfprod  40730  itgsin0pilem1  40735  ibliccsinexp  40736  itgsinexplem1  40739  itgsinexp  40740  iblspltprt  40758  itgsubsticclem  40760  stoweidlem16  40802  stoweidlem18  40804  stoweidlem19  40805  stoweidlem20  40806  stoweidlem22  40808  stoweidlem23  40809  stoweidlem27  40813  stoweidlem31  40817  stoweidlem32  40818  stoweidlem34  40820  stoweidlem35  40821  stoweidlem36  40822  stoweidlem40  40826  stoweidlem41  40827  stoweidlem42  40828  stoweidlem43  40829  stoweidlem44  40830  stoweidlem45  40831  stoweidlem48  40834  stoweidlem51  40837  stoweidlem55  40841  stoweidlem59  40845  stoweidlem60  40846  stoweidlem62  40848  wallispilem5  40855  stirlinglem4  40863  stirlinglem5  40864  stirlinglem8  40867  stirlinglem11  40870  stirlinglem12  40871  stirlinglem13  40872  stirlinglem14  40873  stirlinglem15  40874  stirling  40875  fourierdlem16  40909  fourierdlem21  40914  fourierdlem22  40915  fourierdlem53  40945  fourierdlem68  40960  fourierdlem73  40965  fourierdlem80  40972  fourierdlem89  40981  fourierdlem91  40983  fourierdlem93  40985  fourierdlem103  40995  fourierdlem104  40996  fourierdlem112  41004  fourierdlem115  41007  fourierd  41008  fourierclimd  41009  etransclem48  41068  sge00  41162  sge0revalmpt  41164  sge0f1o  41168  sge0fsummpt  41176  sge0gerp  41181  sge0pnffigt  41182  sge0lefi  41184  sge0ltfirp  41186  sge0resplit  41192  sge0iunmptlemfi  41199  sge0iunmpt  41204  sge0xadd  41221  sge0fsummptf  41222  sge0gtfsumgt  41229  sge0reuz  41233  iundjiun  41246  meaiuninc3v  41270  omeiunltfirp  41305  omeiunlempt  41306  hoicvrrex  41342  ovncvrrp  41350  ovnhoilem1  41387  ovnlecvr2  41396  opnvonmbllem1  41418  iunhoiioolem  41461  pimgtmnf  41504  smfpimltmpt  41527  issmfdmpt  41529  smfconst  41530  smfpimltxrmpt  41539  smflimlem2  41552  smflim  41557  smfpimgtmpt  41561  smfpimgtxrmpt  41564  smfpimcclem  41585  smfpimcc  41586  smflimmpt  41588  smfsupmpt  41593  smfsupxr  41594  smfinfmpt  41597  smflimsuplem2  41599  smflimsuplem7  41604  smflimsupmpt  41607  smfliminfmpt  41610  aacllem  43151
  Copyright terms: Public domain W3C validator