Theorem nfmpt1 5274

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

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Ⅎwnfc 2893  {copab 5228   ↦ cmpt 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-opab 5229  df-mpt 5250

This theorem is referenced by:  nffvmpt1  6931  fvmptss  7041  fvmptd3f  7044  mpteqb  7048  fvmptf  7050  ralrnmptw  7128  ralrnmpt  7130  f1ompt  7145  fompt  7152  f1mpt  7298  fliftfun  7348  rdgsucmptf  8484  rdgsucmptnf  8485  frsucmpt  8494  frsucmptn  8495  dom2lem  9052  mapxpen  9209  cnfcom3clem  9774  ttrclselem1  9794  ttrclselem2  9795  infxpenc2lem2  10089  dfac8clem  10101  acnlem  10117  fin23lem32  10413  axcc3  10507  ac6num  10548  nfcprod1  15956  yonedalem4b  18346  prdsgsum  20023  cayleyhamilton1  22919  neiptopreu  23162  2ndcdisj  23485  ptcnp  23651  cnmpt11  23692  cnmptk2  23715  xkocnv  23843  utopsnneiplem  24277  restmetu  24604  mbfposr  25706  mbfsup  25718  itg1climres  25769  itg2splitlem  25803  itg2split  25804  itg2cnlem1  25816  nfitg1  25829  dvlipcn  26053  lhop2  26074  dvfsumabs  26083  itgparts  26108  itgsubstlem  26109  itgulm2  26470  lgamgulm2  27097  lgseisenlem2  27438  istrkg2ld  28486  cnlnadjlem5  32103  acunirnmpt2  32678  acunirnmpt2f  32679  aciunf1lem  32680  ofpreima  32683  fnpreimac  32689  disjdsct  32714  fpwrelmap  32747  nsgqusf1olem1  33406  nsgqusf1olem3  33408  elrspunidl  33421  fedgmullem2  33643  locfinreflem  33786  prodindf  33987  nfesum1  34004  esumc  34015  esumrnmpt2  34032  esumsup  34053  esumgect  34054  esum2d  34057  sigapildsys  34126  ldgenpisyslem1  34127  voliune  34193  oms0  34262  rrvadd  34417  ballotlem7  34500  breprexplema  34607  cvmcov  35231  rdgssun  37344  exrecfnlem  37345  phpreu  37564  matunitlindflem2  37577  poimirlem16  37596  poimirlem19  37599  itg2addnclem  37631  ftc1anclem5  37657  totbndbnd  37749  pwsgprod  42499  mzpsubmpt  42699  eq0rabdioph  42732  eqrabdioph  42733  aomclem8  43018  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  refsumcn  44930  refsum2cnlem1  44937  disjrnmpt2  45095  disjf1o  45098  disjinfi  45099  choicefi  45107  axccdom  45129  rnmptbd2lem  45157  infnsuprnmpt  45159  rnmptbdlem  45164  rnmptss2  45166  rnmptssbi  45170  supxrleubrnmpt  45321  suprleubrnmpt  45337  infrnmptle  45338  infxrunb3rnmpt  45343  uzub  45346  supminfrnmpt  45360  infxrgelbrnmpt  45369  infrpgernmpt  45380  supminfxrrnmpt  45386  fmuldfeqlem1  45503  fmuldfeq  45504  climneg  45531  climdivf  45533  mullimc  45537  idlimc  45547  sumnnodd  45551  neglimc  45568  addlimc  45569  0ellimcdiv  45570  fnlimfvre  45595  fnlimabslt  45600  climreclmpt  45605  climfveqmpt2  45614  climeldmeqmpt2  45616  climeqmpt  45618  limsupubuz  45634  climinfmpt  45636  limsupubuzmpt  45640  limsupequzmptlem  45649  limsupre2mpt  45651  limsupre3mpt  45655  limsupreuzmpt  45660  liminflelimsuplem  45696  liminfvalxr  45704  liminfvalxrmpt  45707  liminfltlem  45725  liminflbuz2  45736  liminfpnfuz  45737  xlimmnfmpt  45764  xlimpnfmpt  45765  xlimpnfxnegmnf2  45779  cncfmptssg  45792  cncfshift  45795  cncficcgt0  45809  cncfiooicclem1  45814  dvnmul  45864  dvmptfprod  45866  itgsin0pilem1  45871  ibliccsinexp  45872  itgsinexplem1  45875  itgsinexp  45876  iblspltprt  45894  itgsubsticclem  45896  stoweidlem16  45937  stoweidlem18  45939  stoweidlem19  45940  stoweidlem20  45941  stoweidlem22  45943  stoweidlem23  45944  stoweidlem27  45948  stoweidlem31  45952  stoweidlem32  45953  stoweidlem34  45955  stoweidlem35  45956  stoweidlem36  45957  stoweidlem40  45961  stoweidlem41  45962  stoweidlem42  45963  stoweidlem43  45964  stoweidlem44  45965  stoweidlem45  45966  stoweidlem48  45969  stoweidlem51  45972  stoweidlem55  45976  stoweidlem59  45980  stoweidlem60  45981  stoweidlem62  45983  wallispilem5  45990  stirlinglem4  45998  stirlinglem5  45999  stirlinglem8  46002  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  stirling  46010  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem68  46095  fourierdlem73  46100  fourierdlem80  46107  fourierdlem89  46116  fourierdlem91  46118  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fourierdlem112  46139  fourierdlem115  46142  fourierd  46143  fourierclimd  46144  etransclem48  46203  sge00  46297  sge0revalmpt  46299  sge0f1o  46303  sge0fsummpt  46311  sge0gerp  46316  sge0pnffigt  46317  sge0lefi  46319  sge0ltfirp  46321  sge0resplit  46327  sge0iunmptlemfi  46334  sge0iunmpt  46339  sge0xadd  46356  sge0fsummptf  46357  sge0gtfsumgt  46364  sge0reuz  46368  iundjiun  46381  meaiuninc3v  46405  omeiunltfirp  46440  omeiunlempt  46441  hoicvrrex  46477  ovncvrrp  46485  ovnhoilem1  46522  ovnlecvr2  46531  opnvonmbllem1  46553  iunhoiioolem  46596  smfpimltmpt  46667  issmfdmpt  46669  smfconst  46670  smfpimltxrmptf  46679  smflimlem2  46693  smflim  46698  smfpimgtmpt  46702  smfpimgtxrmptf  46705  smfpimcclem  46728  smfpimcc  46729  smflimmpt  46731  smfsupmpt  46736  smfsupxr  46737  smfinfmpt  46740  smflimsuplem2  46742  smflimsuplem7  46747  smflimsupmpt  46750  smfliminfmpt  46753  cfsetsnfsetf  46973  1arymaptfo  48377  2arymaptfo  48388  setrec2mpt  48789  aacllem  48895