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

Theorem nfmpt1 5161
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 5144 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
2 nfopab1 5132 . 2 𝑥{⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
31, 2nfcxfr 2980 1 𝑥(𝑥𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1530  wcel 2107  wnfc 2966  {copab 5125  cmpt 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-opab 5126  df-mpt 5144
This theorem is referenced by:  nffvmpt1  6678  fvmptss  6776  fvmptd3f  6779  mpteqb  6783  fvmptf  6785  ralrnmptw  6856  ralrnmpt  6858  f1ompt  6871  f1mpt  7013  fliftfun  7057  rdgsucmptf  8055  rdgsucmptnf  8056  frsucmpt  8064  frsucmptn  8065  dom2lem  8538  mapxpen  8672  cnfcom3clem  9157  infxpenc2lem2  9435  dfac8clem  9447  acnlem  9463  fin23lem32  9755  axcc3  9849  ac6num  9890  nfcprod1  15254  yonedalem4b  17516  prdsgsum  19021  cayleyhamilton1  21416  neiptopreu  21657  2ndcdisj  21980  ptcnp  22146  cnmpt11  22187  cnmptk2  22210  xkocnv  22338  utopsnneiplem  22771  restmetu  23095  mbfposr  24168  mbfsup  24180  itg1climres  24230  itg2splitlem  24264  itg2split  24265  itg2cnlem1  24277  nfitg1  24289  dvlipcn  24506  lhop2  24527  dvfsumabs  24535  itgparts  24559  itgsubstlem  24560  itgulm2  24912  lgamgulm2  25527  lgseisenlem2  25866  istrkg2ld  26160  cnlnadjlem5  29762  acunirnmpt2  30320  acunirnmpt2f  30321  aciunf1lem  30322  ofpreima  30325  fnpreimac  30331  disjdsct  30351  fpwrelmap  30382  fedgmullem2  30912  locfinreflem  30990  prodindf  31168  nfesum1  31185  esumc  31196  esumrnmpt2  31213  esumsup  31234  esumgect  31235  esum2d  31238  sigapildsys  31307  ldgenpisyslem1  31308  voliune  31374  oms0  31441  rrvadd  31596  ballotlem7  31679  breprexplema  31787  cvmcov  32394  trpredlem1  32950  trpredrec  32961  rdgssun  34528  exrecfnlem  34529  phpreu  34743  matunitlindflem2  34756  poimirlem16  34775  poimirlem19  34778  itg2addnclem  34810  ftc1anclem5  34838  totbndbnd  34935  mzpsubmpt  39205  eq0rabdioph  39238  eqrabdioph  39239  aomclem8  39526  binomcxplemdvbinom  40550  binomcxplemdvsum  40552  binomcxplemnotnn0  40553  refsumcn  41152  refsum2cnlem1  41159  suprnmpt  41295  disjrnmpt2  41314  disjf1o  41317  fompt  41318  disjinfi  41319  choicefi  41328  axccdom  41352  rnmptbd2lem  41385  infnsuprnmpt  41387  rnmptbdlem  41392  rnmptss2  41394  rnmptssbi  41399  supxrleubrnmpt  41544  suprleubrnmpt  41561  infrnmptle  41562  infxrunb3rnmpt  41567  uzub  41570  supminfrnmpt  41584  infxrgelbrnmpt  41595  infrpgernmpt  41606  supminfxrrnmpt  41612  fmuldfeqlem1  41728  fmuldfeq  41729  climneg  41756  climdivf  41758  mullimc  41762  idlimc  41772  sumnnodd  41776  neglimc  41793  addlimc  41794  0ellimcdiv  41795  fnlimfvre  41820  fnlimabslt  41825  climreclmpt  41830  climfveqmpt2  41839  climeldmeqmpt2  41841  climeqmpt  41843  limsupubuz  41859  climinfmpt  41861  limsupubuzmpt  41865  limsupequzmptlem  41874  limsupre2mpt  41876  limsupre3mpt  41880  limsupreuzmpt  41885  liminflelimsuplem  41921  liminfvalxr  41929  liminfvalxrmpt  41932  liminfltlem  41950  liminflbuz2  41961  liminfpnfuz  41962  xlimmnfmpt  41989  xlimpnfmpt  41990  xlimpnfxnegmnf2  42004  cncfmptssg  42018  cncfshift  42022  cncficcgt0  42036  cncfiooicclem1  42041  dvnmul  42093  dvmptfprod  42095  itgsin0pilem1  42100  ibliccsinexp  42101  itgsinexplem1  42104  itgsinexp  42105  iblspltprt  42123  itgsubsticclem  42125  stoweidlem16  42167  stoweidlem18  42169  stoweidlem19  42170  stoweidlem20  42171  stoweidlem22  42173  stoweidlem23  42174  stoweidlem27  42178  stoweidlem31  42182  stoweidlem32  42183  stoweidlem34  42185  stoweidlem35  42186  stoweidlem36  42187  stoweidlem40  42191  stoweidlem41  42192  stoweidlem42  42193  stoweidlem43  42194  stoweidlem44  42195  stoweidlem45  42196  stoweidlem48  42199  stoweidlem51  42202  stoweidlem55  42206  stoweidlem59  42210  stoweidlem60  42211  stoweidlem62  42213  wallispilem5  42220  stirlinglem4  42228  stirlinglem5  42229  stirlinglem8  42232  stirlinglem11  42235  stirlinglem12  42236  stirlinglem13  42237  stirlinglem14  42238  stirlinglem15  42239  stirling  42240  fourierdlem16  42274  fourierdlem21  42279  fourierdlem22  42280  fourierdlem53  42310  fourierdlem68  42325  fourierdlem73  42330  fourierdlem80  42337  fourierdlem89  42346  fourierdlem91  42348  fourierdlem93  42350  fourierdlem103  42360  fourierdlem104  42361  fourierdlem112  42369  fourierdlem115  42372  fourierd  42373  fourierclimd  42374  etransclem48  42433  sge00  42524  sge0revalmpt  42526  sge0f1o  42530  sge0fsummpt  42538  sge0gerp  42543  sge0pnffigt  42544  sge0lefi  42546  sge0ltfirp  42548  sge0resplit  42554  sge0iunmptlemfi  42561  sge0iunmpt  42566  sge0xadd  42583  sge0fsummptf  42584  sge0gtfsumgt  42591  sge0reuz  42595  iundjiun  42608  meaiuninc3v  42632  omeiunltfirp  42667  omeiunlempt  42668  hoicvrrex  42704  ovncvrrp  42712  ovnhoilem1  42749  ovnlecvr2  42758  opnvonmbllem1  42780  iunhoiioolem  42823  pimgtmnf  42866  smfpimltmpt  42889  issmfdmpt  42891  smfconst  42892  smfpimltxrmpt  42901  smflimlem2  42914  smflim  42919  smfpimgtmpt  42923  smfpimgtxrmpt  42926  smfpimcclem  42947  smfpimcc  42948  smflimmpt  42950  smfsupmpt  42955  smfsupxr  42956  smfinfmpt  42959  smflimsuplem2  42961  smflimsuplem7  42966  smflimsupmpt  42969  smfliminfmpt  42972  aacllem  44734
  Copyright terms: Public domain W3C validator