Theorem nfmpt1 5195

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Ⅎwnfc 2881  {copab 5158   ↦ cmpt 5177

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-opab 5159  df-mpt 5178

This theorem is referenced by:  nffvmpt1  6843  fvmptss  6951  fvmptd3f  6954  mpteqb  6958  fvmptf  6960  ralrnmptw  7037  ralrnmpt  7039  f1ompt  7054  fompt  7061  f1mpt  7205  fliftfun  7256  rdgsucmptf  8357  rdgsucmptnf  8358  frsucmpt  8367  frsucmptn  8368  dom2lem  8927  mapxpen  9069  cnfcom3clem  9612  ttrclselem1  9632  ttrclselem2  9633  infxpenc2lem2  9928  dfac8clem  9940  acnlem  9956  fin23lem32  10252  axcc3  10346  ac6num  10387  nfcprod1  15829  yonedalem4b  18197  prdsgsum  19908  pwsgprod  20263  cayleyhamilton1  22834  neiptopreu  23075  2ndcdisj  23398  ptcnp  23564  cnmpt11  23605  cnmptk2  23628  xkocnv  23756  utopsnneiplem  24189  restmetu  24512  mbfposr  25607  mbfsup  25619  itg1climres  25669  itg2splitlem  25703  itg2split  25704  itg2cnlem1  25716  nfitg1  25729  dvlipcn  25953  lhop2  25974  dvfsumabs  25983  itgparts  26008  itgsubstlem  26009  itgulm2  26372  lgamgulm2  27000  lgseisenlem2  27341  istrkg2ld  28481  cnlnadjlem5  32095  acunirnmpt2  32687  acunirnmpt2f  32688  aciunf1lem  32689  ofpreima  32692  fnpreimac  32698  disjdsct  32731  fpwrelmap  32761  prodindf  32893  elrgspnsubrunlem2  33279  nsgqusf1olem1  33443  nsgqusf1olem3  33445  elrspunidl  33458  deg1prod  33613  mplvrpmga  33659  fedgmullem2  33736  locfinreflem  33946  nfesum1  34146  esumc  34157  esumrnmpt2  34174  esumsup  34195  esumgect  34196  esum2d  34199  sigapildsys  34268  ldgenpisyslem1  34269  voliune  34335  oms0  34403  rrvadd  34558  ballotlem7  34642  breprexplema  34736  cvmcov  35406  rdgssun  37522  exrecfnlem  37523  phpreu  37744  matunitlindflem2  37757  poimirlem16  37776  poimirlem19  37779  itg2addnclem  37811  ftc1anclem5  37837  totbndbnd  37929  mzpsubmpt  42927  eq0rabdioph  42960  eqrabdioph  42961  aomclem8  43245  binomcxplemdvbinom  44536  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  refsumcn  45217  refsum2cnlem1  45224  disjrnmpt2  45374  disjf1o  45377  disjinfi  45378  choicefi  45386  axccdom  45408  rnmptbd2lem  45434  infnsuprnmpt  45436  rnmptbdlem  45441  rnmptss2  45443  rnmptssbi  45446  supxrleubrnmpt  45592  suprleubrnmpt  45608  infrnmptle  45609  infxrunb3rnmpt  45614  uzub  45617  supminfrnmpt  45631  infxrgelbrnmpt  45640  infrpgernmpt  45651  supminfxrrnmpt  45657  fmuldfeqlem1  45770  fmuldfeq  45771  climneg  45798  climdivf  45800  mullimc  45804  idlimc  45814  sumnnodd  45818  neglimc  45833  addlimc  45834  0ellimcdiv  45835  fnlimfvre  45860  fnlimabslt  45865  climreclmpt  45870  climfveqmpt2  45879  climeldmeqmpt2  45881  climeqmpt  45883  limsupubuz  45899  climinfmpt  45901  limsupubuzmpt  45905  limsupequzmptlem  45914  limsupre2mpt  45916  limsupre3mpt  45920  limsupreuzmpt  45925  liminflelimsuplem  45961  liminfvalxr  45969  liminfvalxrmpt  45972  liminfltlem  45990  liminflbuz2  46001  liminfpnfuz  46002  xlimmnfmpt  46029  xlimpnfmpt  46030  xlimpnfxnegmnf2  46044  cncfmptssg  46057  cncfshift  46060  cncficcgt0  46074  cncfiooicclem1  46079  dvnmul  46129  dvmptfprod  46131  itgsin0pilem1  46136  ibliccsinexp  46137  itgsinexplem1  46140  itgsinexp  46141  iblspltprt  46159  itgsubsticclem  46161  stoweidlem16  46202  stoweidlem18  46204  stoweidlem19  46205  stoweidlem20  46206  stoweidlem22  46208  stoweidlem23  46209  stoweidlem27  46213  stoweidlem31  46217  stoweidlem32  46218  stoweidlem34  46220  stoweidlem35  46221  stoweidlem36  46222  stoweidlem40  46226  stoweidlem41  46227  stoweidlem42  46228  stoweidlem43  46229  stoweidlem44  46230  stoweidlem45  46231  stoweidlem48  46234  stoweidlem51  46237  stoweidlem55  46241  stoweidlem59  46245  stoweidlem60  46246  stoweidlem62  46248  wallispilem5  46255  stirlinglem4  46263  stirlinglem5  46264  stirlinglem8  46267  stirlinglem11  46270  stirlinglem12  46271  stirlinglem13  46272  stirlinglem14  46273  stirlinglem15  46274  stirling  46275  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem68  46360  fourierdlem73  46365  fourierdlem80  46372  fourierdlem89  46381  fourierdlem91  46383  fourierdlem93  46385  fourierdlem103  46395  fourierdlem104  46396  fourierdlem112  46404  fourierdlem115  46407  fourierd  46408  fourierclimd  46409  etransclem48  46468  sge00  46562  sge0revalmpt  46564  sge0f1o  46568  sge0fsummpt  46576  sge0gerp  46581  sge0pnffigt  46582  sge0lefi  46584  sge0ltfirp  46586  sge0resplit  46592  sge0iunmptlemfi  46599  sge0iunmpt  46604  sge0xadd  46621  sge0fsummptf  46622  sge0gtfsumgt  46629  sge0reuz  46633  iundjiun  46646  meaiuninc3v  46670  omeiunltfirp  46705  omeiunlempt  46706  hoicvrrex  46742  ovncvrrp  46750  ovnhoilem1  46787  ovnlecvr2  46796  opnvonmbllem1  46818  iunhoiioolem  46861  smfpimltmpt  46932  issmfdmpt  46934  smfconst  46935  smfpimltxrmptf  46944  smflimlem2  46958  smflim  46963  smfpimgtmpt  46967  smfpimgtxrmptf  46970  smfpimcclem  46993  smfpimcc  46994  smflimmpt  46996  smfsupmpt  47001  smfsupxr  47002  smfinfmpt  47005  smflimsuplem2  47007  smflimsuplem7  47012  smflimsupmpt  47015  smfliminfmpt  47018  cfsetsnfsetf  47246  1arymaptfo  48831  2arymaptfo  48842  setrec2mpt  49884  aacllem  49988