Theorem nfmpt1 5199

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Ⅎwnfc 2884  {copab 5162   ↦ cmpt 5181

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-opab 5163  df-mpt 5182

This theorem is referenced by:  nffvmpt1  6853  fvmptss  6962  fvmptd3f  6965  mpteqb  6969  fvmptf  6971  ralrnmptw  7048  ralrnmpt  7050  f1ompt  7065  fompt  7072  f1mpt  7217  fliftfun  7268  rdgsucmptf  8369  rdgsucmptnf  8370  frsucmpt  8379  frsucmptn  8380  dom2lem  8941  mapxpen  9083  cnfcom3clem  9626  ttrclselem1  9646  ttrclselem2  9647  infxpenc2lem2  9942  dfac8clem  9954  acnlem  9970  fin23lem32  10266  axcc3  10360  ac6num  10401  nfcprod1  15843  yonedalem4b  18211  prdsgsum  19922  pwsgprod  20277  cayleyhamilton1  22848  neiptopreu  23089  2ndcdisj  23412  ptcnp  23578  cnmpt11  23619  cnmptk2  23642  xkocnv  23770  utopsnneiplem  24203  restmetu  24526  mbfposr  25621  mbfsup  25633  itg1climres  25683  itg2splitlem  25717  itg2split  25718  itg2cnlem1  25730  nfitg1  25743  dvlipcn  25967  lhop2  25988  dvfsumabs  25997  itgparts  26022  itgsubstlem  26023  itgulm2  26386  lgamgulm2  27014  lgseisenlem2  27355  istrkg2ld  28544  cnlnadjlem5  32159  acunirnmpt2  32750  acunirnmpt2f  32751  aciunf1lem  32752  ofpreima  32755  fnpreimac  32760  disjdsct  32793  fpwrelmap  32823  prodindf  32955  suppgsumssiun  33166  elrgspnsubrunlem2  33342  nsgqusf1olem1  33506  nsgqusf1olem3  33508  elrspunidl  33521  deg1prod  33676  mplvrpmga  33722  esplyfval1  33750  fedgmullem2  33808  locfinreflem  34018  nfesum1  34218  esumc  34229  esumrnmpt2  34246  esumsup  34267  esumgect  34268  esum2d  34271  sigapildsys  34340  ldgenpisyslem1  34341  voliune  34407  oms0  34475  rrvadd  34630  ballotlem7  34714  breprexplema  34808  cvmcov  35479  rdgssun  37633  exrecfnlem  37634  phpreu  37855  matunitlindflem2  37868  poimirlem16  37887  poimirlem19  37890  itg2addnclem  37922  ftc1anclem5  37948  totbndbnd  38040  mzpsubmpt  43100  eq0rabdioph  43133  eqrabdioph  43134  aomclem8  43418  binomcxplemdvbinom  44709  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  refsumcn  45390  refsum2cnlem1  45397  disjrnmpt2  45547  disjf1o  45550  disjinfi  45551  choicefi  45558  axccdom  45580  rnmptbd2lem  45606  infnsuprnmpt  45608  rnmptbdlem  45613  rnmptss2  45615  rnmptssbi  45618  supxrleubrnmpt  45764  suprleubrnmpt  45780  infrnmptle  45781  infxrunb3rnmpt  45786  uzub  45789  supminfrnmpt  45803  infxrgelbrnmpt  45812  infrpgernmpt  45823  supminfxrrnmpt  45829  fmuldfeqlem1  45942  fmuldfeq  45943  climneg  45970  climdivf  45972  mullimc  45976  idlimc  45986  sumnnodd  45990  neglimc  46005  addlimc  46006  0ellimcdiv  46007  fnlimfvre  46032  fnlimabslt  46037  climreclmpt  46042  climfveqmpt2  46051  climeldmeqmpt2  46053  climeqmpt  46055  limsupubuz  46071  climinfmpt  46073  limsupubuzmpt  46077  limsupequzmptlem  46086  limsupre2mpt  46088  limsupre3mpt  46092  limsupreuzmpt  46097  liminflelimsuplem  46133  liminfvalxr  46141  liminfvalxrmpt  46144  liminfltlem  46162  liminflbuz2  46173  liminfpnfuz  46174  xlimmnfmpt  46201  xlimpnfmpt  46202  xlimpnfxnegmnf2  46216  cncfmptssg  46229  cncfshift  46232  cncficcgt0  46246  cncfiooicclem1  46251  dvnmul  46301  dvmptfprod  46303  itgsin0pilem1  46308  ibliccsinexp  46309  itgsinexplem1  46312  itgsinexp  46313  iblspltprt  46331  itgsubsticclem  46333  stoweidlem16  46374  stoweidlem18  46376  stoweidlem19  46377  stoweidlem20  46378  stoweidlem22  46380  stoweidlem23  46381  stoweidlem27  46385  stoweidlem31  46389  stoweidlem32  46390  stoweidlem34  46392  stoweidlem35  46393  stoweidlem36  46394  stoweidlem40  46398  stoweidlem41  46399  stoweidlem42  46400  stoweidlem43  46401  stoweidlem44  46402  stoweidlem45  46403  stoweidlem48  46406  stoweidlem51  46409  stoweidlem55  46413  stoweidlem59  46417  stoweidlem60  46418  stoweidlem62  46420  wallispilem5  46427  stirlinglem4  46435  stirlinglem5  46436  stirlinglem8  46439  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  stirlinglem14  46445  stirlinglem15  46446  stirling  46447  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem68  46532  fourierdlem73  46537  fourierdlem80  46544  fourierdlem89  46553  fourierdlem91  46555  fourierdlem93  46557  fourierdlem103  46567  fourierdlem104  46568  fourierdlem112  46576  fourierdlem115  46579  fourierd  46580  fourierclimd  46581  etransclem48  46640  sge00  46734  sge0revalmpt  46736  sge0f1o  46740  sge0fsummpt  46748  sge0gerp  46753  sge0pnffigt  46754  sge0lefi  46756  sge0ltfirp  46758  sge0resplit  46764  sge0iunmptlemfi  46771  sge0iunmpt  46776  sge0xadd  46793  sge0fsummptf  46794  sge0gtfsumgt  46801  sge0reuz  46805  iundjiun  46818  meaiuninc3v  46842  omeiunltfirp  46877  omeiunlempt  46878  hoicvrrex  46914  ovncvrrp  46922  ovnhoilem1  46959  ovnlecvr2  46968  opnvonmbllem1  46990  iunhoiioolem  47033  smfpimltmpt  47104  issmfdmpt  47106  smfconst  47107  smfpimltxrmptf  47116  smflimlem2  47130  smflim  47135  smfpimgtmpt  47139  smfpimgtxrmptf  47142  smfpimcclem  47165  smfpimcc  47166  smflimmpt  47168  smfsupmpt  47173  smfsupxr  47174  smfinfmpt  47177  smflimsuplem2  47179  smflimsuplem7  47184  smflimsupmpt  47187  smfliminfmpt  47190  cfsetsnfsetf  47418  1arymaptfo  49003  2arymaptfo  49014  setrec2mpt  50056  aacllem  50160