Theorem nfmpt1 5185

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

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

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 5149  df-mpt 5168

This theorem is referenced by:  nffvmpt1  6845  fvmptss  6954  fvmptd3f  6957  mpteqb  6961  fvmptf  6963  ralrnmptw  7040  ralrnmpt  7042  f1ompt  7057  fompt  7064  f1mpt  7209  fliftfun  7260  rdgsucmptf  8360  rdgsucmptnf  8361  frsucmpt  8370  frsucmptn  8371  dom2lem  8932  mapxpen  9074  cnfcom3clem  9617  ttrclselem1  9637  ttrclselem2  9638  infxpenc2lem2  9933  dfac8clem  9945  acnlem  9961  fin23lem32  10257  axcc3  10351  ac6num  10392  nfcprod1  15864  yonedalem4b  18233  prdsgsum  19947  pwsgprod  20300  cayleyhamilton1  22867  neiptopreu  23108  2ndcdisj  23431  ptcnp  23597  cnmpt11  23638  cnmptk2  23661  xkocnv  23789  utopsnneiplem  24222  restmetu  24545  mbfposr  25629  mbfsup  25641  itg1climres  25691  itg2splitlem  25725  itg2split  25726  itg2cnlem1  25738  nfitg1  25751  dvlipcn  25971  lhop2  25992  dvfsumabs  26000  itgparts  26024  itgsubstlem  26025  itgulm2  26387  lgamgulm2  27013  lgseisenlem2  27353  istrkg2ld  28542  cnlnadjlem5  32157  acunirnmpt2  32748  acunirnmpt2f  32749  aciunf1lem  32750  ofpreima  32753  fnpreimac  32758  disjdsct  32791  fpwrelmap  32821  prodindf  32937  suppgsumssiun  33148  elrgspnsubrunlem2  33324  nsgqusf1olem1  33488  nsgqusf1olem3  33490  elrspunidl  33503  deg1prod  33658  mplvrpmga  33704  esplyfval1  33732  fedgmullem2  33790  locfinreflem  34000  nfesum1  34200  esumc  34211  esumrnmpt2  34228  esumsup  34249  esumgect  34250  esum2d  34253  sigapildsys  34322  ldgenpisyslem1  34323  voliune  34389  oms0  34457  rrvadd  34612  ballotlem7  34696  breprexplema  34790  cvmcov  35461  rdgssun  37708  exrecfnlem  37709  phpreu  37939  matunitlindflem2  37952  poimirlem16  37971  poimirlem19  37974  itg2addnclem  38006  ftc1anclem5  38032  totbndbnd  38124  mzpsubmpt  43189  eq0rabdioph  43222  eqrabdioph  43223  aomclem8  43507  binomcxplemdvbinom  44798  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  refsumcn  45479  refsum2cnlem1  45486  disjrnmpt2  45636  disjf1o  45639  disjinfi  45640  choicefi  45647  axccdom  45669  rnmptbd2lem  45695  infnsuprnmpt  45697  rnmptbdlem  45702  rnmptss2  45704  rnmptssbi  45707  supxrleubrnmpt  45852  suprleubrnmpt  45868  infrnmptle  45869  infxrunb3rnmpt  45874  uzub  45877  supminfrnmpt  45891  infxrgelbrnmpt  45900  infrpgernmpt  45911  supminfxrrnmpt  45917  fmuldfeqlem1  46030  fmuldfeq  46031  climneg  46058  climdivf  46060  mullimc  46064  idlimc  46074  sumnnodd  46078  neglimc  46093  addlimc  46094  0ellimcdiv  46095  fnlimfvre  46120  fnlimabslt  46125  climreclmpt  46130  climfveqmpt2  46139  climeldmeqmpt2  46141  climeqmpt  46143  limsupubuz  46159  climinfmpt  46161  limsupubuzmpt  46165  limsupequzmptlem  46174  limsupre2mpt  46176  limsupre3mpt  46180  limsupreuzmpt  46185  liminflelimsuplem  46221  liminfvalxr  46229  liminfvalxrmpt  46232  liminfltlem  46250  liminflbuz2  46261  liminfpnfuz  46262  xlimmnfmpt  46289  xlimpnfmpt  46290  xlimpnfxnegmnf2  46304  cncfmptssg  46317  cncfshift  46320  cncficcgt0  46334  cncfiooicclem1  46339  dvnmul  46389  dvmptfprod  46391  itgsin0pilem1  46396  ibliccsinexp  46397  itgsinexplem1  46400  itgsinexp  46401  iblspltprt  46419  itgsubsticclem  46421  stoweidlem16  46462  stoweidlem18  46464  stoweidlem19  46465  stoweidlem20  46466  stoweidlem22  46468  stoweidlem23  46469  stoweidlem27  46473  stoweidlem31  46477  stoweidlem32  46478  stoweidlem34  46480  stoweidlem35  46481  stoweidlem36  46482  stoweidlem40  46486  stoweidlem41  46487  stoweidlem42  46488  stoweidlem43  46489  stoweidlem44  46490  stoweidlem45  46491  stoweidlem48  46494  stoweidlem51  46497  stoweidlem55  46501  stoweidlem59  46505  stoweidlem60  46506  stoweidlem62  46508  wallispilem5  46515  stirlinglem4  46523  stirlinglem5  46524  stirlinglem8  46527  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  stirlinglem14  46533  stirlinglem15  46534  stirling  46535  fourierdlem16  46569  fourierdlem21  46574  fourierdlem22  46575  fourierdlem68  46620  fourierdlem73  46625  fourierdlem80  46632  fourierdlem89  46641  fourierdlem91  46643  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  fourierdlem115  46667  fourierd  46668  fourierclimd  46669  etransclem48  46728  sge00  46822  sge0revalmpt  46824  sge0f1o  46828  sge0fsummpt  46836  sge0gerp  46841  sge0pnffigt  46842  sge0lefi  46844  sge0ltfirp  46846  sge0resplit  46852  sge0iunmptlemfi  46859  sge0iunmpt  46864  sge0xadd  46881  sge0fsummptf  46882  sge0gtfsumgt  46889  sge0reuz  46893  iundjiun  46906  meaiuninc3v  46930  omeiunltfirp  46965  omeiunlempt  46966  hoicvrrex  47002  ovncvrrp  47010  ovnhoilem1  47047  ovnlecvr2  47056  opnvonmbllem1  47078  iunhoiioolem  47121  smfpimltmpt  47192  issmfdmpt  47194  smfconst  47195  smfpimltxrmptf  47204  smflimlem2  47218  smflim  47223  smfpimgtmpt  47227  smfpimgtxrmptf  47230  smfpimcclem  47253  smfpimcc  47254  smflimmpt  47256  smfsupmpt  47261  smfsupxr  47262  smfinfmpt  47265  smflimsuplem2  47267  smflimsuplem7  47272  smflimsupmpt  47275  smfliminfmpt  47278  cfsetsnfsetf  47518  1arymaptfo  49131  2arymaptfo  49142  setrec2mpt  50184  aacllem  50288