Theorem nfmpt1 5128

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

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Ⅎwnfc 2936  {copab 5092   ↦ cmpt 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-opab 5093  df-mpt 5111

This theorem is referenced by:  nffvmpt1  6656  fvmptss  6757  fvmptd3f  6760  mpteqb  6764  fvmptf  6766  ralrnmptw  6837  ralrnmpt  6839  f1ompt  6852  f1mpt  6997  fliftfun  7044  rdgsucmptf  8047  rdgsucmptnf  8048  frsucmpt  8056  frsucmptn  8057  dom2lem  8532  mapxpen  8667  cnfcom3clem  9152  infxpenc2lem2  9431  dfac8clem  9443  acnlem  9459  fin23lem32  9755  axcc3  9849  ac6num  9890  nfcprod1  15256  yonedalem4b  17518  prdsgsum  19094  cayleyhamilton1  21497  neiptopreu  21738  2ndcdisj  22061  ptcnp  22227  cnmpt11  22268  cnmptk2  22291  xkocnv  22419  utopsnneiplem  22853  restmetu  23177  mbfposr  24256  mbfsup  24268  itg1climres  24318  itg2splitlem  24352  itg2split  24353  itg2cnlem1  24365  nfitg1  24377  dvlipcn  24597  lhop2  24618  dvfsumabs  24626  itgparts  24650  itgsubstlem  24651  itgulm2  25004  lgamgulm2  25621  lgseisenlem2  25960  istrkg2ld  26254  cnlnadjlem5  29854  acunirnmpt2  30423  acunirnmpt2f  30424  aciunf1lem  30425  ofpreima  30428  fnpreimac  30434  disjdsct  30462  fpwrelmap  30495  elrspunidl  31014  fedgmullem2  31114  locfinreflem  31193  prodindf  31392  nfesum1  31409  esumc  31420  esumrnmpt2  31437  esumsup  31458  esumgect  31459  esum2d  31462  sigapildsys  31531  ldgenpisyslem1  31532  voliune  31598  oms0  31665  rrvadd  31820  ballotlem7  31903  breprexplema  32011  cvmcov  32623  trpredlem1  33179  trpredrec  33190  rdgssun  34795  exrecfnlem  34796  phpreu  35041  matunitlindflem2  35054  poimirlem16  35073  poimirlem19  35076  itg2addnclem  35108  ftc1anclem5  35134  totbndbnd  35227  mzpsubmpt  39684  eq0rabdioph  39717  eqrabdioph  39718  aomclem8  40005  binomcxplemdvbinom  41057  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  refsumcn  41659  refsum2cnlem1  41666  suprnmpt  41798  disjrnmpt2  41815  disjf1o  41818  fompt  41819  disjinfi  41820  choicefi  41829  axccdom  41853  rnmptbd2lem  41886  infnsuprnmpt  41888  rnmptbdlem  41893  rnmptss2  41895  rnmptssbi  41899  supxrleubrnmpt  42043  suprleubrnmpt  42059  infrnmptle  42060  infxrunb3rnmpt  42065  uzub  42068  supminfrnmpt  42082  infxrgelbrnmpt  42093  infrpgernmpt  42104  supminfxrrnmpt  42110  fmuldfeqlem1  42224  fmuldfeq  42225  climneg  42252  climdivf  42254  mullimc  42258  idlimc  42268  sumnnodd  42272  neglimc  42289  addlimc  42290  0ellimcdiv  42291  fnlimfvre  42316  fnlimabslt  42321  climreclmpt  42326  climfveqmpt2  42335  climeldmeqmpt2  42337  climeqmpt  42339  limsupubuz  42355  climinfmpt  42357  limsupubuzmpt  42361  limsupequzmptlem  42370  limsupre2mpt  42372  limsupre3mpt  42376  limsupreuzmpt  42381  liminflelimsuplem  42417  liminfvalxr  42425  liminfvalxrmpt  42428  liminfltlem  42446  liminflbuz2  42457  liminfpnfuz  42458  xlimmnfmpt  42485  xlimpnfmpt  42486  xlimpnfxnegmnf2  42500  cncfmptssg  42513  cncfshift  42516  cncficcgt0  42530  cncfiooicclem1  42535  dvnmul  42585  dvmptfprod  42587  itgsin0pilem1  42592  ibliccsinexp  42593  itgsinexplem1  42596  itgsinexp  42597  iblspltprt  42615  itgsubsticclem  42617  stoweidlem16  42658  stoweidlem18  42660  stoweidlem19  42661  stoweidlem20  42662  stoweidlem22  42664  stoweidlem23  42665  stoweidlem27  42669  stoweidlem31  42673  stoweidlem32  42674  stoweidlem34  42676  stoweidlem35  42677  stoweidlem36  42678  stoweidlem40  42682  stoweidlem41  42683  stoweidlem42  42684  stoweidlem43  42685  stoweidlem44  42686  stoweidlem45  42687  stoweidlem48  42690  stoweidlem51  42693  stoweidlem55  42697  stoweidlem59  42701  stoweidlem60  42702  stoweidlem62  42704  wallispilem5  42711  stirlinglem4  42719  stirlinglem5  42720  stirlinglem8  42723  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  stirlinglem14  42729  stirlinglem15  42730  stirling  42731  fourierdlem16  42765  fourierdlem21  42770  fourierdlem22  42771  fourierdlem53  42801  fourierdlem68  42816  fourierdlem73  42821  fourierdlem80  42828  fourierdlem89  42837  fourierdlem91  42839  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  fourierdlem112  42860  fourierdlem115  42863  fourierd  42864  fourierclimd  42865  etransclem48  42924  sge00  43015  sge0revalmpt  43017  sge0f1o  43021  sge0fsummpt  43029  sge0gerp  43034  sge0pnffigt  43035  sge0lefi  43037  sge0ltfirp  43039  sge0resplit  43045  sge0iunmptlemfi  43052  sge0iunmpt  43057  sge0xadd  43074  sge0fsummptf  43075  sge0gtfsumgt  43082  sge0reuz  43086  iundjiun  43099  meaiuninc3v  43123  omeiunltfirp  43158  omeiunlempt  43159  hoicvrrex  43195  ovncvrrp  43203  ovnhoilem1  43240  ovnlecvr2  43249  opnvonmbllem1  43271  iunhoiioolem  43314  pimgtmnf  43357  smfpimltmpt  43380  issmfdmpt  43382  smfconst  43383  smfpimltxrmpt  43392  smflimlem2  43405  smflim  43410  smfpimgtmpt  43414  smfpimgtxrmpt  43417  smfpimcclem  43438  smfpimcc  43439  smflimmpt  43441  smfsupmpt  43446  smfsupxr  43447  smfinfmpt  43450  smflimsuplem2  43452  smflimsuplem7  43457  smflimsupmpt  43460  smfliminfmpt  43463  1arymaptfo  45057  2arymaptfo  45068  aacllem  45329