Theorem nfmpt1 5188

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Ⅎwnfc 2879  {copab 5151   ↦ cmpt 5170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-opab 5152  df-mpt 5171

This theorem is referenced by:  nffvmpt1  6833  fvmptss  6941  fvmptd3f  6944  mpteqb  6948  fvmptf  6950  ralrnmptw  7027  ralrnmpt  7029  f1ompt  7044  fompt  7051  f1mpt  7195  fliftfun  7246  rdgsucmptf  8347  rdgsucmptnf  8348  frsucmpt  8357  frsucmptn  8358  dom2lem  8914  mapxpen  9056  cnfcom3clem  9595  ttrclselem1  9615  ttrclselem2  9616  infxpenc2lem2  9911  dfac8clem  9923  acnlem  9939  fin23lem32  10235  axcc3  10329  ac6num  10370  nfcprod1  15815  yonedalem4b  18182  prdsgsum  19893  cayleyhamilton1  22807  neiptopreu  23048  2ndcdisj  23371  ptcnp  23537  cnmpt11  23578  cnmptk2  23601  xkocnv  23729  utopsnneiplem  24162  restmetu  24485  mbfposr  25580  mbfsup  25592  itg1climres  25642  itg2splitlem  25676  itg2split  25677  itg2cnlem1  25689  nfitg1  25702  dvlipcn  25926  lhop2  25947  dvfsumabs  25956  itgparts  25981  itgsubstlem  25982  itgulm2  26345  lgamgulm2  26973  lgseisenlem2  27314  istrkg2ld  28438  cnlnadjlem5  32051  acunirnmpt2  32642  acunirnmpt2f  32643  aciunf1lem  32644  ofpreima  32647  fnpreimac  32653  disjdsct  32684  fpwrelmap  32716  prodindf  32844  elrgspnsubrunlem2  33215  nsgqusf1olem1  33378  nsgqusf1olem3  33380  elrspunidl  33393  mplvrpmga  33575  fedgmullem2  33643  locfinreflem  33853  nfesum1  34053  esumc  34064  esumrnmpt2  34081  esumsup  34102  esumgect  34103  esum2d  34106  sigapildsys  34175  ldgenpisyslem1  34176  voliune  34242  oms0  34310  rrvadd  34465  ballotlem7  34549  breprexplema  34643  cvmcov  35307  rdgssun  37420  exrecfnlem  37421  phpreu  37652  matunitlindflem2  37665  poimirlem16  37684  poimirlem19  37687  itg2addnclem  37719  ftc1anclem5  37745  totbndbnd  37837  pwsgprod  42585  mzpsubmpt  42784  eq0rabdioph  42817  eqrabdioph  42818  aomclem8  43102  binomcxplemdvbinom  44394  binomcxplemdvsum  44396  binomcxplemnotnn0  44397  refsumcn  45075  refsum2cnlem1  45082  disjrnmpt2  45233  disjf1o  45236  disjinfi  45237  choicefi  45245  axccdom  45267  rnmptbd2lem  45293  infnsuprnmpt  45295  rnmptbdlem  45300  rnmptss2  45302  rnmptssbi  45305  supxrleubrnmpt  45452  suprleubrnmpt  45468  infrnmptle  45469  infxrunb3rnmpt  45474  uzub  45477  supminfrnmpt  45491  infxrgelbrnmpt  45500  infrpgernmpt  45511  supminfxrrnmpt  45517  fmuldfeqlem1  45630  fmuldfeq  45631  climneg  45658  climdivf  45660  mullimc  45664  idlimc  45674  sumnnodd  45678  neglimc  45693  addlimc  45694  0ellimcdiv  45695  fnlimfvre  45720  fnlimabslt  45725  climreclmpt  45730  climfveqmpt2  45739  climeldmeqmpt2  45741  climeqmpt  45743  limsupubuz  45759  climinfmpt  45761  limsupubuzmpt  45765  limsupequzmptlem  45774  limsupre2mpt  45776  limsupre3mpt  45780  limsupreuzmpt  45785  liminflelimsuplem  45821  liminfvalxr  45829  liminfvalxrmpt  45832  liminfltlem  45850  liminflbuz2  45861  liminfpnfuz  45862  xlimmnfmpt  45889  xlimpnfmpt  45890  xlimpnfxnegmnf2  45904  cncfmptssg  45917  cncfshift  45920  cncficcgt0  45934  cncfiooicclem1  45939  dvnmul  45989  dvmptfprod  45991  itgsin0pilem1  45996  ibliccsinexp  45997  itgsinexplem1  46000  itgsinexp  46001  iblspltprt  46019  itgsubsticclem  46021  stoweidlem16  46062  stoweidlem18  46064  stoweidlem19  46065  stoweidlem20  46066  stoweidlem22  46068  stoweidlem23  46069  stoweidlem27  46073  stoweidlem31  46077  stoweidlem32  46078  stoweidlem34  46080  stoweidlem35  46081  stoweidlem36  46082  stoweidlem40  46086  stoweidlem41  46087  stoweidlem42  46088  stoweidlem43  46089  stoweidlem44  46090  stoweidlem45  46091  stoweidlem48  46094  stoweidlem51  46097  stoweidlem55  46101  stoweidlem59  46105  stoweidlem60  46106  stoweidlem62  46108  wallispilem5  46115  stirlinglem4  46123  stirlinglem5  46124  stirlinglem8  46127  stirlinglem11  46130  stirlinglem12  46131  stirlinglem13  46132  stirlinglem14  46133  stirlinglem15  46134  stirling  46135  fourierdlem16  46169  fourierdlem21  46174  fourierdlem22  46175  fourierdlem68  46220  fourierdlem73  46225  fourierdlem80  46232  fourierdlem89  46241  fourierdlem91  46243  fourierdlem93  46245  fourierdlem103  46255  fourierdlem104  46256  fourierdlem112  46264  fourierdlem115  46267  fourierd  46268  fourierclimd  46269  etransclem48  46328  sge00  46422  sge0revalmpt  46424  sge0f1o  46428  sge0fsummpt  46436  sge0gerp  46441  sge0pnffigt  46442  sge0lefi  46444  sge0ltfirp  46446  sge0resplit  46452  sge0iunmptlemfi  46459  sge0iunmpt  46464  sge0xadd  46481  sge0fsummptf  46482  sge0gtfsumgt  46489  sge0reuz  46493  iundjiun  46506  meaiuninc3v  46530  omeiunltfirp  46565  omeiunlempt  46566  hoicvrrex  46602  ovncvrrp  46610  ovnhoilem1  46647  ovnlecvr2  46656  opnvonmbllem1  46678  iunhoiioolem  46721  smfpimltmpt  46792  issmfdmpt  46794  smfconst  46795  smfpimltxrmptf  46804  smflimlem2  46818  smflim  46823  smfpimgtmpt  46827  smfpimgtxrmptf  46830  smfpimcclem  46853  smfpimcc  46854  smflimmpt  46856  smfsupmpt  46861  smfsupxr  46862  smfinfmpt  46865  smflimsuplem2  46867  smflimsuplem7  46872  smflimsupmpt  46875  smfliminfmpt  46878  cfsetsnfsetf  47097  1arymaptfo  48683  2arymaptfo  48694  setrec2mpt  49737  aacllem  49841