Theorem nfmpt1 5204

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Ⅎwnfc 2908  {copab 5167   ↦ cmpt 5186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-opab 5168  df-mpt 5187

This theorem is used by:  nffvmpt1  6894  fvmptss  7004  fvmptd3f  7007  mpteqb  7011  fvmptf  7013  ralrnmptw  7092  ralrnmpt  7094  f1ompt  7109  fompt  7116  f1mpt  7263  fliftfun  7318  rdgsucmptf  8429  rdgsucmptnf  8430  frsucmpt  8439  frsucmptn  8440  dom2lem  9012  mapxpen  9155  cnfcom3clem  9699  ttrclselem1  9719  ttrclselem2  9720  infxpenc2lem2  10092  dfac8clem  10104  acnlem  10120  fin23lem32  10415  axcc3  10509  ac6num  10550  nfcprod1  16070  yonedalem4b  18443  prdsgsum  20188  pwsgprod  20552  matunitlindflem2  22988  cayleyhamilton1  23203  neiptopreu  23444  2ndcdisj  23768  ptcnp  23934  cnmpt11  23975  cnmptk2  23998  xkocnv  24126  utopsnneiplem  24559  restmetu  24882  mbfposr  25966  mbfsup  25978  itg1climres  26028  itg2splitlem  26062  itg2split  26063  itg2cnlem1  26075  nfitg1  26087  dvlipcn  26307  lhop2  26328  dvfsumabs  26336  itgparts  26360  itgsubstlem  26361  itgulm2  26729  lgamgulm2  27356  lgseisenlem2  27696  istrkg2ld  28915  cnlnadjlem5  32666  acunirnmpt2  33247  acunirnmpt2f  33248  aciunf1lem  33249  ofpreima  33252  fnpreimac  33257  disjdsct  33289  fpwrelmap  33318  prodindf  33422  suppgsumssiun  33626  elrgspnsubrunlem2  33802  nsgqusf1olem1  33957  nsgqusf1olem3  33959  elrspunidl  33971  deg1prod  34108  mplvrpmga  34170  esplyfval1  34198  fedgmullem2  34255  locfinreflem  34465  nfesum1  34665  esumc  34676  esumrnmpt2  34693  esumsup  34714  esumgect  34715  esum2d  34718  sigapildsys  34788  ldgenpisyslem1  34789  voliune  34855  oms0  34922  rrvadd  35077  ballotlem7  35161  breprexplema  35252  cvmcov  36007  rdgssun  38281  exrecfnlem  38282  phpreu  38507  poimirlem16  38534  poimirlem19  38537  itg2addnclem  38569  ftc1anclem5  38595  totbndbnd  38703  mzpsubmpt  43733  eq0rabdioph  43766  eqrabdioph  43767  aomclem8  44047  binomcxplemdvbinom  45322  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  refsumcn  46016  refsum2cnlem1  46023  disjrnmpt2  46172  disjf1o  46175  disjinfi  46176  choicefi  46183  axccdom  46204  rnmptbd2lem  46229  infnsuprnmpt  46231  rnmptbdlem  46236  rnmptss2  46238  rnmptssbi  46241  supxrleubrnmpt  46385  suprleubrnmpt  46401  infrnmptle  46402  infxrunb3rnmpt  46407  uzub  46410  supminfrnmpt  46424  infxrgelbrnmpt  46433  infrpgernmpt  46444  supminfxrrnmpt  46450  fmuldfeqlem1  46563  fmuldfeq  46564  climneg  46591  climdivf  46593  mullimc  46597  idlimc  46607  sumnnodd  46611  neglimc  46626  addlimc  46627  0ellimcdiv  46628  fnlimfvre  46653  fnlimabslt  46658  climreclmpt  46663  climfveqmpt2  46672  climeldmeqmpt2  46674  climeqmpt  46676  limsupubuz  46692  climinfmpt  46694  limsupubuzmpt  46698  limsupequzmptlem  46707  limsupre2mpt  46709  limsupre3mpt  46713  limsupreuzmpt  46718  liminflelimsuplem  46754  liminfvalxr  46762  liminfvalxrmpt  46765  liminfltlem  46783  liminflbuz2  46794  liminfpnfuz  46795  xlimmnfmpt  46822  xlimpnfmpt  46823  xlimpnfxnegmnf2  46837  cncfmptssg  46850  cncfshift  46853  cncficcgt0  46867  cncfiooicclem1  46872  dvnmul  46922  dvmptfprod  46924  itgsin0pilem1  46929  ibliccsinexp  46930  itgsinexplem1  46933  itgsinexp  46934  iblspltprt  46952  itgsubsticclem  46954  stoweidlem16  46995  stoweidlem18  46997  stoweidlem19  46998  stoweidlem20  46999  stoweidlem22  47001  stoweidlem23  47002  stoweidlem27  47006  stoweidlem31  47010  stoweidlem32  47011  stoweidlem34  47013  stoweidlem35  47014  stoweidlem36  47015  stoweidlem40  47019  stoweidlem41  47020  stoweidlem42  47021  stoweidlem43  47022  stoweidlem44  47023  stoweidlem45  47024  stoweidlem48  47027  stoweidlem51  47030  stoweidlem55  47034  stoweidlem59  47038  stoweidlem60  47039  stoweidlem62  47041  wallispilem5  47048  stirlinglem4  47056  stirlinglem5  47057  stirlinglem8  47060  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  stirling  47068  fourierdlem16  47102  fourierdlem21  47107  fourierdlem22  47108  fourierdlem68  47153  fourierdlem73  47158  fourierdlem80  47165  fourierdlem89  47174  fourierdlem91  47176  fourierdlem93  47178  fourierdlem103  47188  fourierdlem104  47189  fourierdlem112  47197  fourierdlem115  47200  fourierd  47201  fourierclimd  47202  etransclem48  47261  sge00  47355  sge0revalmpt  47357  sge0f1o  47361  sge0fsummpt  47369  sge0gerp  47374  sge0pnffigt  47375  sge0lefi  47377  sge0ltfirp  47379  sge0resplit  47385  sge0iunmptlemfi  47392  sge0iunmpt  47397  sge0xadd  47414  sge0fsummptf  47415  sge0gtfsumgt  47422  sge0reuz  47426  iundjiun  47439  meaiuninc3v  47463  omeiunltfirp  47498  omeiunlempt  47499  hoicvrrex  47535  ovncvrrp  47543  ovnhoilem1  47580  ovnlecvr2  47589  opnvonmbllem1  47611  iunhoiioolem  47654  smfpimltmpt  47725  issmfdmpt  47727  smfconst  47728  smfpimltxrmptf  47737  smflimlem2  47751  smflim  47756  smfpimgtmpt  47760  smfpimgtxrmptf  47763  smfpimcclem  47786  smfpimcc  47787  smflimmpt  47789  smfsupmpt  47794  smfsupxr  47795  smfinfmpt  47798  smflimsuplem2  47800  smflimsuplem7  47805  smflimsupmpt  47808  smfliminfmpt  47811  cfsetsnfsetf  48097  1arymaptfo  49724  2arymaptfo  49735  setrec2mpt  50759  aacllem  50908